Аксіоми виводу типу комбінатора

Лекція 7

Лекція 6

 

· алфавіт;

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

· аксіоми;

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

 

 

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

2. змінні;

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

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

 

 

Константи c1 , c2, ...

Змінні 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 Логическое значение
... ... ... ...