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

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

Лекція 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);

 

 

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

 

  1. Явний перелік елементів множини даного типу
  2. Тип 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.