КАТЕГОРИИ: Архитектура-(3434)Астрономия-(809)Биология-(7483)Биотехнологии-(1457)Военное дело-(14632)Высокие технологии-(1363)География-(913)Геология-(1438)Государство-(451)Демография-(1065)Дом-(47672)Журналистика и СМИ-(912)Изобретательство-(14524)Иностранные языки-(4268)Информатика-(17799)Искусство-(1338)История-(13644)Компьютеры-(11121)Косметика-(55)Кулинария-(373)Культура-(8427)Лингвистика-(374)Литература-(1642)Маркетинг-(23702)Математика-(16968)Машиностроение-(1700)Медицина-(12668)Менеджмент-(24684)Механика-(15423)Науковедение-(506)Образование-(11852)Охрана труда-(3308)Педагогика-(5571)Полиграфия-(1312)Политика-(7869)Право-(5454)Приборостроение-(1369)Программирование-(2801)Производство-(97182)Промышленность-(8706)Психология-(18388)Религия-(3217)Связь-(10668)Сельское хозяйство-(299)Социология-(6455)Спорт-(42831)Строительство-(4793)Торговля-(5050)Транспорт-(2929)Туризм-(1568)Физика-(3942)Философия-(17015)Финансы-(26596)Химия-(22929)Экология-(12095)Экономика-(9961)Электроника-(8441)Электротехника-(4623)Энергетика-(12629)Юриспруденция-(1492)Ядерная техника-(1748) |
Аксіоми виводу типу комбінатора
Чиста система типів Лекція 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 | <змінна> | (<комбінаторний терм> <комбінаторний терм>)
Деякі корисні співвідношення для комбінаторів
механізм редукції 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).
Визначення функцій, що реалізують характеристики деяких з базисних комбінаторів:
тип 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>
А à c:s
#M ||- T – приписування типу
1. Базисні типи d1, d2, d3 2. Базисний тип – тип 3. a, b, то f(a)=b, a à b
Ієрархія типів = <похідний тип> ={<базисні типи> … }
тип 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; Просмотров: 362; Нарушение авторских прав?; Мы поможем в написании вашей работы! Нам важно ваше мнение! Был ли полезен опубликованный материал? Да | Нет |