Лекція 5

· алфавіт;

· твердження;

· аксіоми;

· правила виводу.

1. константи;

2. змінні;

3. вирази (або терми);

4. спеціальні символи.

Константи c₁, c₂,...

Змінні x, y,...

Вирази (терми) M, N,...

Спеціальні символи "(", ")", "."

1) вираз (λx.M) є допустимим ламбда- термом;

2) вираз (MN) є допустимим ламбда- термом.

аксіоми відношення конвертованості:

(a) λx.a = λz.[z/x]a; підстановка терма z

(β) (λx.a)b = [b/x]a. редукція виразу

правила виводу термів конвертованості:

(μ) якщо a=b, то ca=cb;

(ν) якщо a=b, то ac=bc;

(ξ) якщо a=b, то lx.a=lx.b;

(ρ) a=a (рефлексивність);

(σ) якщо a=b, то b=a (симетричність);

(τ) якщо a=b і b=c, то a=c (транзитивність).

Домовленості про читання і обробку ламбда- виразів.

xy = (xy), xyz = ((xy)z),...

(xy) = xy, ((xy)z) = xyz,...

λxy.M = (λx.(λy.M)), λxyz.M = (λx.(λy.(λz.M))),...

ламбда- терми:

1.	x;	змінна
2.	1;	константа
3.	lx.x;	ламбда-абстракція (тотожність)
4.	lx.x + 1;	функція інкремента
5.	(lx.x + 1)2 = [2/x](x + 1) = 2+1 = 3;	підстановка відповідно аксіомі ()
6.	A $ b	недопустимий

фрагменти SML-програм, що відповідають наведеним вище допустимим ламбда- термам:

1. x (змінна, тип якої визначається в процесі трансляції на етапі контроля типизації у відповідності з виводом типів);

2. 1 (константа);

3. fn x => x (функція тотожності);

4. fn x => x+1 (функція інкремента);

5. (fn x => x+1) 2 (обчислення значення функції, в результатом виконання якої є ціле число 3).

fun f x = b;

fun f x = 1+x;

f 4;

f 2 + 3; ((f2)+3, а не f(2+3))

Дата добавления: 2014-01-07