Базис термов

Возникает вопрос: существует ли конечный набор комбинаторов, посредством которого можно выразить произвольный терм комбинаторной логики? Оказывается, что ответ на поставленный вопрос утвердителен, причем введенные аксиомы и правила вывода обеспечивают весьма лаконичный набор такого рода.

Необходимость продолжения рассуждений приводит нас к понятию базиса.

Определение 6.3. Базисом (минимальным) называется множество (минимальной мощности) комбинаторов, через элементы которого может быть выражен произвольный комбинатор.

Оказывается, можно доказать, что:

1. базис термов для комбинаторной логики действительно существует (причем существует бесконечное множество возможных базисов);

2. для любого базиса справедливо, что он обеспечивает представление произвольного комбинаторного терма (в силу свойства полноты, которым обладает система комбинаторной логики);

3. минимальный базис состоит всего из двух "инструкций"- комбинаторов, например, {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).

Разложение в базисе аналогично программированию на языке базисных инструкций.

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

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

Для более подробного самостоятельного ознакомления с тематикой лекции рекомендуется следующий список источников: [32, 43, 44, 76].

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

В данной лекции исследуются принципы, математическое основание и выразительные возможности теории типов и типизированной комбинаторной логики - математической формализации, моделирующей типы выражений в языках программирования.

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

Рассмотрим построение системы типизации на основе комбинаторной логики.

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