Аксіоми

Крок індукції

Базис

Порядок конструювання термів

Алфавіт

Лекція 4. Лямбда-числення, як формалізація мови функціонального програмування

· алфавіт;

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

· аксіоми;

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

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

2. змінні;

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

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

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

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

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

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

Константа і змінна є лямбда-термом

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 (транзитивність).

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

1. Аплікація -

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

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

3. Абстракція

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

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

1.	x;	змінна
2.	1;	константа
3.	λx.x;	ламбда-абстракція (тотожність)
4.	λx.x + 1;	функція інкремента
5.	(λx.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