МФСП, 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 • 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
        <i>^lr → length(lr) + 1
      end

Задач. Опр. функцию Pascal, гненер. тр. Пскаля д урвня n вкл. Результат --- список списков. Например:

<<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 • j in <2..i-1>>^<1>>

Задача. Реализовать функцию rev, кторая взвр. реверсивную версию списка.

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

(стандартный тип text в rsl н смом деле text=char×)

Для тких типов тр. опр. функцию is_on, проверяющую, встречется ли данне слово на странице

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))

Определить number_of, пдсчитывающую количество вхождений слоов в страницу

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•j:Nat; • p(i)(j)=w ∧ i∈ p ∧ ∈p(i)}