2 Постановка задачи: о связном предъявлении теории информатики и практики программирования в теме исполнения для теоретического мышления. 13 (стр. 11 из 25)

Комбинаторная логика. Созидается теория, в которой фиксируется, что значит равенство термов. Фиксируется посредством доказательства. Подразумеваемая структура: A = <A, *, c₁,¼,c_m>. Язык: термы, построенные из переменных, K, S посредством операции *. Формулы: равенства термов. Аксиомы: t = t для атомарных термов. St₁t₂t₃ = t₁t₃(t₂t₃) Kt₁t₂ = t₁ для произвольных термов. Правила вывода:

Доказуемость: последовательность равенств a₁, a₂,¼, a_n называется доказательством a_n, если a_i - аксиома, либо имеются j, k < i такие, что a_i получается из a_j и a_k по правилу вывода.

{278 Гоген} Эквациональная логика, которая по существу является логикой подстановки “равных вместо равных”, составляет фундаментальное ядро (???) функционального программирования.

Вопрос о непротиворечивости сводится к доказательству того факта, что невозможно вывести все формулы соответствующего языка. Например, формулу K = S. Действительно, если K = S, то

То есть t₁= t₂(дал произвольные).

Исчисление редукций. Создается теория, в которой фиксируется, что значит редуцируется терм к другому. Фиксируется посредством доказательства. Язык: термы как в комбинаторной логике. Формулы: высказывания о редуцируемости t₁ ® t₁Аксиомы: t ® t для атомарных термов. St₁t₂t₃ ® t₁t₃(t₂t₃) Kt₁t₂ ® t₁ для произвольных термов. Правила вывода:

Редуцируемость: как доказуемость в комбинаторной логике.

Исчисление конверсий. Еще более общее понятие (эквивалентное одновременной конверсии). Язык: термы комбинаторной логики. Формулы: t₁ ||® t₂ (||® семантика этого знака - редуцируется равенством). Аксиомы: t ||® t для атомарных термов. St₁t₂t₃ ||® t₁t₃(t₂t₃) Kt₁t₂ ||® t₁ для произвольных термов. Правила вывода:

Конвертируемость: как доказуемость в комбинаторной логике.

Индукцией по длине доказательства можем доказать, что

Лемма 1. t₁®t₂Û t₁||®t₁₁* , t₁₁||®t₁₂, ¼, t_1n||®t₂. {Справа - это не тоже, что t₁||®t₂}.

Можем получить теорему Чёрча-Россера: если m=n в комбинаторной логике, тогда $z (m®z Ù n®z), причем строится z эффективно по доказательству m=n. (При доказательстве теоремы используются похожие свойства для редукции и конверсии. Для редукции: если (a®m Ù a®n) Þ $z (m®z Ù n®z). Для конверсии аналогично.)

Теорема. S=K недоказуемо в комбинаторной логике.

Доказательство: от противного. Пусть S=K доказуемо. Тогда $z (S®z Ù K®z) по теореме Чёрча-Россера. Тогда существует последовательность конверсий

S||®c₁₁, ¼, c_1n||®z, что невозможно, т.к. S||®S и только.

3 Модели из термов (эрбрановская модель).

Подобные модели конкретны в той же степени, что и объекты классической математики вообще. Показав, что комбинаторная логика непротиворечива, мы получили разбиение термов комбинаторной логики на классы эквивалентности посредством доказуемости.

Итак, t~t¢ Û t=t¢ - можно доказать. Эта эквивалентность, по определению комбинаторной логики (t₁=t₂ Þ zt₁=zt₂и t₁z=t₂z), является даже конгруэнтностью относительно операции *. То есть если t₁=t₁¢ и t₂=t₂¢ Þ t₁*t₂=t₁¢*t₂¢. Действительно, t₁=t₁¢ Þ t₁*t₂=t₁¢*t₂, t₂=t₂¢ Þ t₁¢*t₂=t₁¢*t₂¢.Тогда t₁*t₂=t₁¢*t₂¢.

Итак, определения.

Модель из термов. T = термы комбинаторной логики, t~t¢ Û t=t¢ доказуемо. Пусть `t = {t¢ | t~t¢}. Заметим, что отношение эквивалентности является конгруэнцией для *, т.е. t₁~t₁¢, t₂~t₂¢ влечет t₁*t₂~ t₁¢*t₂¢ Система <`A, *, `S, `K> является комбинаторной алгеброй, где

`A = {`t | tÎT}:

.` Она называется моделью из термов.

Сравним конструкцию модели из термов с моделью поля рациональных чисел. Сделаем все последовательно. Рассмотрим натуральные числа N={1,2,¼} как абелеву полугруппу с дополнением, т.е.

<N, +>; x+y=y+x; x+(y+z)=(x+y)+z; x+y¹x;

x¹y Þ $z (x+z=y Ú x=y+z).

Перейдем к целым числам.

Если n £ m Þ вычитание не может быть натуральным числом; обозначим его временно символом n Q m: n Q m = x Û n = x+m.

Если мы хотим сохранить аксиомы сложения, тогда

m+k = x+(m+k), kÎN

m-k = x+m-k, 1 £ k < min(m,n), т.е.

(*)

Например, (1Q3) = (2Q4) = (3Q5) = (4Q6) = (5Q7) = ¼

Класс эквивалентности (*) можем задать в виде

(**) (n₁Qm₁) + (n₂Qm₂) Û n₁+m₂ + n₂+m₁

Рассмотрим теперь всевозможные выражения nQm, n,mÎN с законом отождествления (**). Посмотрим на сложение

т.е. складывать можем покомпонентно.

Посмотрим на вычитание

(nQm) Q (n¢Qm¢) Û yQz. Как обычно, выразим через сложение (nQm) = (yQz) + (n¢Qm¢) = (y+n¢) Q (z+m¢), т.е.

Это нужно, так как мы хотим представить (yQz) = (y+n¢+m¢)Q(z+n¢+m¢) = (n+n¢+k)Q(m+n¢+k) = (n+m¢)Q(m+n¢). Итак, (nQm)Q(n¢Qm¢) = (n+m¢)Q(m+n¢).

Рассмотрим класс эквивалентности, выберем для них формы представления и нормальные формы. Введем символ 0.

Итак, целые положительные представляются (n,0),

целые отрицательные представляются (0,n),

ноль представляется (0,0).

Классы эквивалентности образуют группу по сложению, она изоморфна множеству отрицательных чисел Z.

Установление равенства представителей целых чисел устанавливается или приводимостью к нормальной форме или по свойству

(m₁,n₁) = (m₂,n₂) Û m₁+n₂= m₂+n₁.

Сравним с установлением равенства двух термов комбинаторной алгебры. Значительно сложнее. Дело в том, что вопрос о доказуемости равенства t = t¢ алгоритмически неразрешим.

4 Графиковые модели - существование комбинаторных алгебр.

Значение таких моделей, как подчеркивает Д. Скотт, в том, что они действительно делают приведенные теории исчислениями. Через интерпретацию фиксируется “истинность” равенства двух термов.

Попытаемся реализовать элементы комбина¢торной алгебры в виде множеств. Будем рассматривать (по Дирихле) график функции ¦

F = {<x, ¦(x)> | x Î D¦}.

Применение F{a} = {b | $xÎ{a}. <x, b>ÎF}.

В общем случае MÑN = {y | $xÎN. <x,y>ÎM}.

Вспомним сложность, возникающую из-за несоответствия мощностей. Поэтому опираемся на конечные множества. Здесь, в конечности множеств, конечно же “твердый орешек” и достижение Скотта.

Итак, M*N =_Df{y | $xÍN. <x,y>ÎM Ù x - конечное}.

Чтобы легче воспринимать функциональные связи пишем (x®y) вместо <x,y>. Попробуем смастерить комбинатор K. (на множествах, вопрос об Универсуме пока открыт)

KMN=M={m | mÎM}

Хотелось бы иметь FM=N, это получим, если F = {(Æ®y) | yÎM}.

KM должен давать F, тогда K = {{y}®(Æ®y) | yÎУниверсума}.

Действительно,

Пусть Универсум формируется на основе множества A={a,b,c}. Кроме A он должен также содержать функции. Рассмотрим K{a}{b} = {{Æ®a}}*{b} = {a}.

Попробуем смастерить комбинатор S: SMNL = ML (NL). Рассмотрим выражение ML (NL), которое дает некоторое {s | “условие”}. Затем по “условию” попробуем восстановить S. {где ML применяют к NL}.

M*L*(N*L) = {непустому значению} = {s | $rÎN*L . (r®s)ÎM*L} =

= {s | $rÍN*L, $tÍL . (t®(r®s))ÎM} =

= {s | $n³0 $r₁,¼,r_nÎ Универсума $s₁,¼,s_nÎL . (s₁®r₁)ÎN Ù¼Ù(s_n®r_n)ÎN Ù (t®({r₁,¼,r_n}®s))ÎM}.

Тогда за S можем взять множество

S={{t®({r₁,¼,r_n}®s)} ® ({s₁®r₁,¼,s_n®r_n} ® (tÈs₁È¼Ès_n®s)) | n³0, r₁,¼,r_nÎУниверсума}.

Проверим правильность выбора S на простом примере

Чуть изменим SMN{a} = {{a,c}®c}*{a} = Æ,

Легко убедиться, что S¹K. Действительно,

Графиковые модели. Пусть A¹Æ. Тогда G_o(A)=A, G_n₊₁(A)=G_n(A)È{(a®y) | yÎG_n(A), aÍG_n(A), a - конечно}. Пусть

, и пусть B = 2^G(A)- множество-степень множества G(A). {MÍG(A) Û MÎB} К = {{y}®(Æ®y) | yÎG(A)}. /*yÎG(A), а не B, но KÎB*/ S={{t®({r₁,¼,r_n}®s)} ® ({s₁®r₁,¼,s_n®r_n} ® (tÈs₁È¼Ès_n®s)) | n³0, r₁,¼,r_nÎG(A); t, s₁,¼,s_nÎB и конечны}. Итак, B = <B, *, S, K> - комбинаторная алгебра.

Универсум G(a) определяется довольно сложно. Приведем его в общем определении графиковой модели.