МФСП, 04 семинар (от 22 сентября)

Материал из eSyr's wiki.

Спи ски

Спискм в RSL нз. упорядч. типизир. нбр эл-тов, эл-иы могут пвторяться. Списк в угловых скбкх, прядок вжен, все элементы дного типа

<1, 3, 1, 5, 4>
<false, true>

Для спискв, кк и для всех типов в rsl пр. две перации: =, ≠

Для список опр. дв типа: T-list, T-inflist (по ANSI); T*, T^ω

Определён пустой список: <>

пр. синтаксис <v1..vn>

Опр. синтксис: <expr|limit>

Пример:

<2*n|n in <0..3>>

Список может быть опр. для лдюбго ип, не олько бзового: мнжества, списка...

Для того, чтобы добрться д эл-та, исп. перация index, "()", в которой ук. номер эл-та:

<1,4,5,6>(2) = 4
<2,5,3>,<3,1>>(2) = <3,1>
<2,5,3>,<3,1>>(2)(2) = 1

Операции со списками:

Конктенция:

Конк. мжно применять только к кнеч. спискм, второй эл-т мжет быть и конеч, и беск. Рез-т соотв. типа
l1^l2

Head: Первый элемент

hd: T^ω стрелочк с влной T
hd<> = chaos

Tail: Хвст

tl: T^ω стрпелчк с волной T^ω
tl<> = chaos

Len: длина списка

len:T^ω стрелочк с влной Nat
len<n|n &dot; is_prime> == chaos

elems: Элементы

elems: T^ω стрелочк с волнлй T-infset

inds: Индексы

inds: T^ω стрелочк с волнлй Nat-infset 

Задача: пр. функцию length, которя выч. длину списка

value
  length: T* → Nat
    length(l) == if l ≠ <> then 1 + length(tl l) else 0 end

  length2: T* → Nat 
    length2(l) == card inds l

Конструкция case:

case cond of
  pattern1 → expr1
  pattern2 → expr2
  ...
  _ → def_expr
end

Как это исп. для работы со спискми (на том же примере):

value
  length: T* → Nat
    length(l) ==
      case l of
        <> → 0
        ^lr → length(lr) + 1
      end

<<1>,
 <1,1>,
 <1,2,1>,
 <1,3,3,1>,
 <1,4,6,4,1>>

type
  T1={i | i:Nat ˙ i ≥ 1}

value
  pascal:T1 → (T1*)*
    pascal(i) == if i=1 then <<1>> else pascal(i-1)^<<1>^<pascal(i-1)(i-1)(j)+pascal(i-1)(i-1)(j-)|j:T1 &dot; j in <2..i-1>>^<1>>

value
  rev:T* → T*
    rev(l) == if l = <> then <> else rev(tl l)^ hd l end

value
  rev:T* → T*
    rev(l) == <l(len(l)+1-n)|n in <1..len(n)>>

type
  Page=Line*,
  Line=Word*,
  Word

value
  is_on: Word × Page → Bool
    is_on(w,p) == if p=<> then False else w ∈ elems hd p ∨ is_on(w, tl p) end

  is_on: Word × Page → Bool
    is_on(w,p) == ∃ i : Nat ˙ (i ∈ {1..len(p)}) ∧ (w ∈ elems p(i))

value
  number_of: Word × Page → Nat
    number_of(w,p) → if p=<> then 0 else number_of_line(w,l) + number_of(w, tl p)

  number_of_line: Word × Line → Nat
    number_o_line(w,l) → if l=<> then 0 else (if w=hd l then 1 else 0) + number_of_line(w, tl l)


  number_of: Word × Page → Nat
    number_of(w,p) → {(i,j)|(i:Nat&dot;j:Nat; &dot; p(i)(j)=w ∧ i∈ p ∧ ∈p(i)}