Аксіоми виводу типу комбінатора
Чиста система типів
Лекція 6. Теорія типів і комбінаторна логіка
Лекція 6. Теорія типів і комбінаторна логіка
Базис термів
Крок індукції
Базис
Лекція 5. Комбінаторна логіка як формальна система
λx.А
· алфавіт;
· твердження;
· аксіоми;
· правила виводу.
1. константи;
2. змінні;
3. комбінаторні вирази (або терми);
4. спеціальні символи.
Константи c1 , c2, ...
Змінні 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);
Способи визначення типів:
- Явний перелік елементів множини даного типу
- Тип T – властивості елементів d з предметної сфери D
T = {d: D | Ψ}
<S, A, R>
А à c:s
#M ||- T – приписування типу
1. Базисні типи d1 , d2 , d3
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.