Аксіоми виводу типу комбінатора. 3. комбінаторні вирази (або терми);

Лекція 7

Лекція 6

· алфавіт;

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

· аксіоми;

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

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

2. змінні;

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

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

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

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

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

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

вираз (MN) є допустимим комбінаторним термом.

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

(I) Ix = x; існування комбінатора (функції) тотожності

(K) Kxy = x; існування комбінатора (функції) взяття першої проекції

(S) Sxyz = xz(yz). комбінатор - конектор

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

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

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

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

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

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

XY = (XY), XYZ = ((XY)Z),...

(XY) = XY, ((XY)Z) = XYZ,...

БНФ -опис комбінатора:

<комбінатор>::= K | S | (<комбінатор> <комбінатор>)

БНФ -опис терма комбінаторної логіки, можливо із змінними:

<комбінаторний терм>::= K | S | <змінна> |

(<комбінаторний терм> <комбінаторний терм>)

Деякі корисні співвідношення для комбінаторів

(I)	I a = a;	комбінатор тотожності
(K)	К ab = a;	канцелятор (комбінатор взяття першої проекції)
(S)	S abc = ac(bc);	комбінатор-конектор
(B)	B abc = a(bc);	комбінатор композиції
(C)	C abc = acb;	пермутація (перестановка)
(W)	W xy = xyy.	дублювання аргументів

механізм редукції

SKKx = (за правилом S) Kx(Kx) = (за правилом K) x.

звідки, з урахуванняи аксіом і правила (I),

I = SKK

Розкладання термів в базисі {K,S} для розглянутих вище комбінаторів:

B = S(KS)K; W = SS(K(SKK)); C = S(BBS)(KK).

тип a приписаний комбінатору X тоді і лише тоді, коли це твердження отримано з таких аксіом:

(FI) ||- #(I) = (a,a),

(FK) ||- #(K) = (a,(b,a)) = (a,b,a),

(FS) ||- #(S) = ((a,(b,c)), ((a, b)(a,c)))

і правила виводу

(F) если ||- #(X) = (a,b) и ||- #(U) = a,

то ||- #(XU) = b.

визначення функцій

fun Ix = x;

fun Kxy = x;

fun Sxyz = xz(yz);

T = {d: D|Ψ}

<S, A, R>

#M ||- T – приписування типу

Аксіома (I)	Ix = x	існування комбінатора (функції) тотожності
Аксіома (K)	Kxy = x	існування комбінатора (функції) взяття першої проекції
Аксіома (S)	Sxyz = xz(yz)	попарного зв'язування третього елементу с першими двома

(FI) ||- #(I) = (a,a), тип тотожності

(FK) ||- #(K) = (a,(b,a)) = (a,b,a), тип канцелятора

(FS) ||- #(S) = ((a,(b,c)), ((a, b)(a,c))) тип зв'язування (конектора)

(F) якщо ||- #(X) = (a,b) и ||- #(U) = a,

то ||- #(XU) = b.

базисні типи:

int - цілі числа;

string - рядки символів;

bool - логічні значення.

let

val Id = fn x => x

in (Id 3, Id true)

end

fn Id => (Id 3, Id true)) (fn x => x)

Приклад 1.

val x=2*3;

val x = 6: int

Приклад 2.

1+2;

3: int

Приклад 3.

fun add (x: int)(y: int) = x+y;

val add = fn: int -> int -> int

Приклад 4.

add 1 3;

val it = 4: int

Приклад 5.

val f = add 1;

val f = fn: int -> int

f 4;

val it = 5: int

Приклад 6.

hd [1,2,3];

val it = 1: int

тип (int list -> int).

Приклад 7.

hd [true, false, true, false];

val it = true: bool

тип bool list -> bool

Приклад 8.

hd [(1,2)(3,4),(5,6)];

val it = (1,2): int*int

тип ((int*int)list -> (int*int)).

Таблиця 7.1. Відображення типів мови програмування SML в типи ієрархії CTS

№	Тип	Класс.NET	Пояснение
	int	System.Int32	Целое число
	string	System.String	Строка
	bool	System.Boolean	Логическое значение
...	...	...	...

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