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

Чиста система типів

Лекція 6. Теорія типів і комбінаторна логіка

Лекція 6. Теорія типів і комбінаторна логіка

Базис термів

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

Базис

Лекція 5. Комбінаторна логіка як формальна система

λx.А

· алфавіт;

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

· аксіоми;

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

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

2. змінні;

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

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

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

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

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

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

Константа і змінна є комбінаторним термом

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} – мінімальний; {I,K,S}; {I,B,C,S}; {B,W,K}

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

B = S(KS)K;

W = SS(K(SKK));

C = S(BBS)(KK).

Визначення функцій, що реалізують характеристики деяких з базисних комбінаторів:

fun Ix = x;	Функція I реалізує комбінатор тотожності I
fun Kxy = x;	функція K - комбінатор-канцелятор K
fun Sxyz = xz(yz);	функція S - комбінатор-конектор S

тип 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);

Способи визначення типів:

1. Явний перелік елементів множини даного типу
2. Тип T – властивості елементів d з предметної сфери D

T = {d: D | Ψ}

<S, A, R>

А à c:s

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

1. Базисні типи d₁, d₂, d₃

2. Базисний тип – тип

3. a, b, то f(a)=b, a à b

Ієрархія типів = <похідний тип> ={<базисні типи> … }

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

тип 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.

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