глава на потока и за дясна част т.н. отложен обект

В Scheme потоците се определят с помощта на двуаргументен конструктор cons-stream и едноаргументни селектори head и tail. За тях е изпълнено следното: (head (cons-stream a b)) се оценява с оценката на a, (tail (cons-stream a b)) се оценява с оценката на b.

Конструкторът cons-stream създава поток с първи елемент оценката на първия аргумент и опашка – отложен обект, свързан с втория аргумент, оценката на който трябва да е поток.

Селекторът head извлича първият елемент на потока, селекторът tail извлича опашката на потока. Празният поток се означава с атома the-empty-stream. Предикатът empty-stream? се използва за проверка за празен поток.

Пример (дефиниране на поток с елементи 1 и 2):

(define stream (cons-stream 1 (cons-stream 2 the-empty-stream))).

Дотук съществува известна прилика между потоците и списъците, но както ще видим по-нататък разликата е принципна. Възможно е, например, да създаваме потоци с безкрайно много елементи.
Основната идея в реализацията на потоците е те да не се конструират изцяло. С други думи, при конструиране на поток се пресмята само първия елемент на потока, а конструирането на останалата част от потока се отлага докато не се поиска достъп до нея. Това се постига с помощта на така нареченето отложено оценяване, което се осигурява чрез специалната форма delay и вградената функция force.

Специалната форма delay има следния синтаксис: (delay <израз>).

Тя не оценява аргумента си. В резултат на оценяване на обръщение към delay в текущата среда се създава “пакетирана” форма на израза, която позволява той да се оцени чак когато е необходимо.

Може да се счита, че delay е такава специална форма, че извикването (delay <израз>) е еквивалентно на извикването (lambda () <израз>).

Вградената функция force има следния синтаксис:

(force <отложен_израз>). Тя връща оценката на израза, чието оценяване преди това е било отложено с delay. Казваме още, че отложеният израз се форсира. В съответствие с горното съображение за delay, извикването (force <отложен_израз>) е еквивалентно на извикването (<отложен_израз>).

При тези дефиниции оценката на (force (delay x)) винаги съвпада с оценката на x.
Конструкторът cons-stream може да се реализира като специална форма, която не оценява втория си аргумент и обръщението

(cons-stream a b) е еквивалентно на обръщението (cons a (delay b)). При това положение селекторите head и tail се дефинират по следния начин:

(define (head stream) (car stream))

(define (tail stream) (force (cdr stream)))

(define (append-streams s1 s2)

(if (empty-stream? s1) s2

(cons-stream (head s1) (append-streams (tail s1) s2))))

Тази процедура е приложима само когато s1 е краен поток, s2 може да е безкраен поток.
Извеждане на поток:

(define (print-stream s)

(if (empty-stream? s) (newline)

(begin

(display “ “)

(print-stream (tail s)))))

Тази процедура е приложима само когато s е краен поток.

(действа подобно на filter при списъци):

(define (filter-stream s pred)

(cond ((empty-stream? s) s)

((pred (head s)) (cons-stream (head s)

(filter-stream (tail s) pred)))

(else (filter-stream (tail s) pred))))

Тази процедура е приложима дори когато s е безкраен поток.

Сумиране на два целочислени потока (допълнени с нули, ако е необходимо):

(define (add-streams s1 s2)

(cond ((empty-stream? s1) s2)

((empty-stream? s2) s1)

(else (cons-stream (+ (head s1) (head s2))

(add-streams (tail s1) (tail s2)))))

Процедурата е приложима дори когато и двата потока s1 и s2 са безкрайни.

Функция за съставяне на краен поток от естествените числа в даден интервал:

(define (enum-stream a b)

(if (> a b) the-empty-stream

(cons-stream a (enum-stream (+ a 1) b))))

Потоците се използват тогава, когато е нужна структура, от която трябва да се използва някаква предварително неизвестна част. Формирането на цялата структура би било неефективно, ако тази структура има голям брой елементи и дори невъзможно, ако структурата е с безброй много елементи.

При първия подход потокът се генерира чрез рекурсивна процедура, при втория подход потокът се генерира чрез рекурсия по отношение на генерираната негова част.

Ще разгледаме два примера за неявно генериране на безкраен поток.

Генериране на безкраен поток от естествените числа:

(define (ints_from_n n)

(cons-stream n (ints_from_n (+ n 1))))

(define integers (ints_from 0))

Генериране на безкраен поток от числата на Фибоначи:

(define (fibgen a b)

(cons-stream a (fibgen b (+ a b))))

(define fibs (fibgen 1 1))

И в двата случая не се достига до безкрайна рекурсия, поради реализацията на потоците чрез отложено оценяване.

Накрая ще разгледаме примери за явно генериране на безкраен поток.

Генериране на безкраен поток от единици:

(define ones (cons-stream 1 ones))

Генериране на безкраен поток от естествените числа:

(define ints (cons-stream 0 (add-streams ones ints)))

Тук идеята е, че потокът (tail ints) се получава като към всеки елемент на ints се добави единица.

Генериране на безкраен поток от числата на Фибоначи:

(define fibs (cons-stream 1

(cons-stream 1

(add-streams (tail fibs) fibs))))

Тук идеята е, че потокът (tail (tail fibs)) се получава като се съберат поелементно потоците fibs и (tail fibs).
15. Семантична характеризация на логическите формули и програми.
Дадена е една азбука, наречена базисна, която съдържа измежду своите символи отварящата кръгла скоба (ляв ограничител) (, затварящата кръгла скоба (десен ограничител) ) и запетаята (разделител) ,. Фиксираме множество  от думи над тази азбука, което е обединение на следните множества:

• 
   (множество на променливите) – изброимо безкрайно множество от думи;
  
• 
  за всяко цяло n  0, множество Ф_n от думи – множество на n-местните функционални символи;
  
• 
  за всяко цяло n  0, множество П_n от думи – множество на n-местните предикатни символи;
  
• 
  непразно множество Л на логическите символи.
  

• 
  множеството Л се състои точно от 7 различни думи, които ще означаваме с not, true, fail, and, or, for_all, for_some;
  
• 
  Л   = ;
  
• 
  Л  Ф_n =  за всяко n  0;
  
• 
  Л  П_n =  за всяко n  0;
  
• 
    Ф_n =  за всяко n  0;
  
• 
    П_n =  за всяко n  0;
  
• 
  Ф_n  П_n =  за всяко n  0;
  
• 
  думите от всички множества Л, , Ф_n (n  0) П_n (n  0) не съдържат скоби и запетаи, откъдето следва, че префиксните изрази над  имат еднозначен синтактичен анализ.
  

0-местните функционални символи още наричаме константи.

степен Dⁿ в { 0, 1}. При това, под 0-местен предикат разбираме елемент на { 0, 1}.

Под структура разбираме наредена тройка от непразно множество D, което наричаме носител на структурата,

редица { _n }, където за всяко цяло n  0 _n e интерпретация на символите от Ф_n в D и редица { _n}, където за всяко цяло n  0 _n е интерпретация на символите от П_n в D.

Нека S = < D, { _n }, { _n} > е структура.

Ако f  Ф_n, то вместо _n (f) ще пишем f ^S.

Ако p  П_n, то вместо _n (p) пишем p^S.

Въведеното означение не е съвсем точно – например една дума може да е едновременно функционален и предикатен символ (на различен брой аргументи). Затова понякога е удобно да се въведе допълнително ограничение - всяка дума от  да попада най-много в едно от множествата Ф_n и П_n, n = 0, 1, …, но ние засега няма да въвеждаме такова ограничение – ще считаме, че интерпретацията се подразбира от контекста.

База: Всяка константа е терм. Всяка променлива е терм.

Предположение: Нека f  Ф_n, n > 0 и T₁, T₂, …, T_n са термове.

Стъпка: Тогава думата f (T₁, T₂, …, T_n) е терм.

База: Ако T е константа, определяме VAR (T) = . Ако T е променлива, определяме VAR (T) = { T}.

Предположение: Нека T = f (T₁, T₂, …, T_n), където T₁, T₂, …, T_n са термове и VAR (T₁), VAR (T₂), …, VAR (T_n) са дефинирани.

Стъпка: Тогава дефинираме

VAR (T) = VAR (T₁)  VAR (T₂)  …  VAR (T_n).
Твърдение: За всеки терм T, VAR (T) е крайно множество.

Доказателство: Тривиална индукция по построението на T.

Ще дадем още една индуктивна дефиниция за затворен терм.

База: Всички константи са затворени термове.

Предположение: Нека f  Ф_n, n > 0 и T₁, …, T_n са затворени термове.

Стъпка: Тогава f (T₁, …, T_n) е затворен терм.
Твърдение: Двете дефиниции за затворен терм са еквивалентни.

Доказателство: За едната посока с индукция се показва, че всеки затворен в смисъл на индуктивната дефиниция терм има празно множество от променливи, за другата посока с индукция се показва, че всеки терм е или с непразно множество от променливи или е затворен в смисъла на индуктивната дефиниция.

₀, ₁, …; съответно на функционалните и на предикатните символи.

На всеки затворен терм T съпоставяме елемент от D, който наричаме стойност на затворения терм T в S.

Означаваме стойността на T в S с T ^S.

Дефиницията е с индукция по построението на T.

База: Ако T е константа, то T ^S = ₀ (T).

Предположение: Нека T = f (T₁, T₂, …, T_n), където T₁, …, T_n са затворени термове и T₁^S, …, T_n^S са дефинирани.

Стъпка: Тогава T ^S = f ^S (T₁^S, …, T_n^S).

Нека v е оценка на променливите в S. На всеки терм T

съпоставяме елемент от D, който наричаме стойност на терма T в S при оценката v.

Означаваме стойността на T в S при оценката v с T ^{S, v}.

Дефиницията е с индукция по построението на T.

База: Ако T е константа, T ^{S, v} = ₀ (T) = T ^S. Ако T е променлива,

T ^{S, v} = v (T).

Предположение: Нека T = f (T₁, T₂, …, T_n) и T₁^{S, v}, T₂^{S, v}, …, T_n^{S, v} са дефинирани.

Стъпка: Тогава T ^{S, v} = f ^S (T₁^{S, v}, T₂^{S, v}, …, T_n^{S, v}).
Твърдение: Ако T е затворен терм, то T ^{S, v} = T ^S за всяка оценка v.

Доказателство: Тривиална индукция по T.

Доказателство: Тривиална индукция по T.

Ако p  П_n, n > 0 и T₁, T₂, …, T_n са термове, то p (T₁, T₂, …, T_n) е атомарна формула. Ако p  П₀, то p е атомарна формула.

VAR (A) = VAR (T₁)  VAR (T₂)  … VAR (T_n).

Ако A  П₀, VAR (A) = .

Очевидно, VAR (A) е крайно множество.

Очевидно е, че атомарната формула A е затворена 

A  П₀ или A = p (T₁, T₂, …, T_n), където T₁, T₂, …, T_n са затворени термове.
Фиксираме структура S с носител D и интерпретации ₀, ₁, …;

₀, ₁, …; съответно на функционалните и на предикатните символи.

от { 0, 1}, наречен стойност на A в S.

Стойността на A бележим с A^S.

По дефиниция, ако A = p (T₁, …, T_n), то A^S = p^S (T₁^S, …, T_n^S).

Ако A  П₀, то A^S = ₀ (A).

Ако A^S = 1, казваме че A е вярна в S,

ако A^S = 0, казваме че A не е вярна в S.

Нека v е оценка на променливите. На всяка атомарна формула А съпоставяме елемент от { 0, 1}, наречен стойност на A в S при оценката v. Бележим стойността на A в S при оценката v с A^{S, v}.

По дефиниция, ако A = p (T₁, T₂, …, T_n),

то A^{S, v} = p^S (T₁^{S, v}, T₂^{S, v}, …, T_n^{S, v}). Ако A  П₀, то A^{S, v} = ₀ (A) = A^S.

Доказателство: Прилагаме съответното твърдение от термове.

Доказателство: Прилагаме съответното твърдение от термове.

База: Всяка атомарна формула е логическа формула.

Думите true, fail са логически формули.

Предположение: Нека F е логическа формула, n > 1 и

F₁, F₂, …, F_n са логически формули.

Стъпка: Думата not(F) е логическа формула – нарича се отрицание на F. Думата and(F₁, F₂, …, F_n) е логическа формула – нарича се конюнкция на формулите F₁, F₂, …, F_n. Думата

or(F₁, F₂, …, F_n) е логическа формула – нарича се дизюнкция на формулите F₁, F₂, …, F_n. Ако x е променлива, думата

for_all(x, F) е логическа формула – нарича се генерализация на F по x. Ако x е променлива, думата for_some(x, F) е логическа формула – нарича се екзистенциализация на F по x.

логическата формула not(F) ще означаваме с F,

логическата формула and(F₁, F₂, …, F_n) ще означаваме с

F₁ & F₂ & … & F_n,

логическата формула or(F₁, F₂, …, F_n) ще означаваме с

F₁  F₂  …  F_n,

логическата формула for_all(x, F) ще означаваме с x F,

логическата формула for_some(x, F) ще означаваме с x F.

База: Ако F е атомарна формула, то VAR (F) е вече дефинирано.

Ако F = true или F = fail, дефинираме VAR (F) = .

Предположение: Нека F, F₁, …, F_n (n > 1) са формули и VAR (F),

VAR (F₁), …, VAR (F_n) са вече дефинирани.

Стъпка: Дефинираме VAR (F) = VAR (F),

VAR (F₁ & F₂ & …& F_n) = VAR (F₁)  VAR (F₂)  … VAR (F_n),

VAR (F₁  F₂  …  F_n) = VAR (F₁)  VAR (F₂)  … VAR (F_n),

VAR (x F) = VAR (F)  { x}, VAR (x F) = VAR (F)  { x}.
С индукция по построението тривиално се проверява, че за всяка формула F, VAR (F) е крайно множество.
Нека S е структура, F е формула.

За формулата F дефинираме множество на свободните променливите на F – FVAR (F) с индукция по построението.

База: Ако F е атомарна формула, то FVAR (F) = VAR (F).

Ако F = true или F = fail, дефинираме FVAR (F) = .

Предположение: Нека F, F₁, …, F_n (n > 1) са формули и FVAR (F),

FVAR (F₁), …, FVAR (F_n) са вече дефинирани.

Стъпка: Дефинираме FVAR (F) = FVAR (F),

FVAR (F₁ & F₂ & … F_n) = FVAR (F₁)  FVAR (F₂)  … FVAR (F_n),

FVAR (F₁  F₂  …  F_n) = FVAR (F₁)  FVAR (F₂)  … FVAR (F_n),

FVAR (x F) = FVAR (F)\{ x}, FVAR (x F) = FVAR (F)\{ x}.

Ако A е атомарна формула, то FVAR (A) = VAR (A), така че за атомарни формули тази дефиниция съвпада с предишната дефиниция за затвореност.

База: Всяка атомарна формула е безкванторна формула.

Думите true, fail са безкванторни формули.

Предположение: Нека F е безкванторна формула, n > 1 и

F₁, F₂, …, F_n са безкванторни формули.

Стъпка: Тогава F, F₁ & F₂ & …& F_n, F₁  F₂  … F_n са безкванторни формули.

Доказателство: Тривиална индукция по F.

₀, ₁, …; съответно на функционалните и на предикатните символи.

Дефинираме оценка u по следния начин:

Оценката u наричаме модификация на v върху x чрез d.

Модификацията бележим по следния начин: v[x : d].
Нека v е произволна оценка. На всяка логическа формула F съпоставяме елемент от { 0, 1}, наречен стойност на F в S при оценката v. Стойността на F в S при оценка v означаваме с F ^{S, v}.

Дефинираме индуктивно стойност на формулата F при произволна оценка v.

База: Ако F е атомарна формула, то при произволна оценка v

F ^{S, v} е вече дефинирано.

Ако F = true, то при произволна оценка v, F ^{S, v} = 1.

Ако F = fail, то при произволна оценка v, F ^{S, v} = 0.

Предположение: Нека F ^{S, v}, F₁^{S, v}, F₂^{S, v}, …, F_n^{S, v} са дефинирани за произволна оценка v.

Стъпка: Тогава за произволна оценка v дефинираме:

(F)^{S, v} = 1 – F ^{S, v},

(F₁ & F₂ & …& F_n)^{S, v} = min { F₁^{S, v}, F₂^{S, v}, …, F_n^{S, v}},

(F₁  F₂  …  F_n)^{S, v} = max { F₁^{S, v}, F₂^{S, v}, …, F_n^{S, v}},

(x F)^{S, v} = min { F ^{S, v[x : d]} |d  D},

(x F)^{S, v} = max { F ^{S, v[x : d]} |d  D}.
Казваме, че F е вярна в S при оценката v, ако F ^{S, v} = 1.

Tова записваме още по следния начин: S, v F.

Казваме, че F е невярна в S при оценката v, ако F ^{S, v} = 0.

Tова записваме още по следния начин: S, v  F.