Приписывание типа комбинатору неподвижной точки.

Ya = a(Ya)

a^α(Ya)^β Y^{α→ β}

a ^β→γ

Y –функция, работающая по схеме: получив на входе в качестве аргумента функцию, на выходе Y формирует неподвижную точку этой  функции.

Замечание:

Y в типизированном исчислении не существует.

Вычисление выражений при помощи комбинаторной логики.

Выражение вида:

let x=plus in x(4(x where x=3))

можно переписать так: (λx.x 4((λx.x)3))+

Здесь λx.x = I

      λx.C = KC, x FV(C)

      λx.PQ = S(λx.P)(λx.Q)

 

λx.x4((λx.x)3) = λx.((x4)(I3)) = S(λx.x4)(λx.(I3)) = S(S(λx.x)(λx.4))(K(I3)) =

S(SI(K4))(K(I3)) =>

S(SI(K4))(K(I#))+ = SI(K4)+(K(I3)+) = I+((K4)+)(K(I3)+) = I+(K4+)(K(I3)+) = +4(I3) = +43

Контрольные вопросы

1. В чем Вы видите преимущества типизированных систем перед бестиповыми?
2. Задайте типы основных комбинаторов.
3. Какое правило вывода позволяет приписывать тип аппликации типизированных объектов?
4. Приведите примеры комбинаторов, которым невозможно приписать тип.
5. Вычислите выражение let x = 12 in *((x where x=7)(y where y=x))

Реализация языков программирования

Общая схема реализации функциональных языков

ML, JScript, Hope, Lisp.

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

Пример. Выражения на языке Lisp.

((lambda(xy)(apply+(list(xy)))34) = (λx.λy(+(xy)))34

Hо в Lisp сложение можно записать как (+34).

 

Есть множество функциональных языков (ФЯ). Все они легко переводятся в λ-исчисление.

	Редукция графа (РГ) λ-исчисление интерпретаторы

 

  

                        

ML LISP HOPE

Результат (Нормальная форма).

λ-исчисление (расширен- ное)

Суперкомбинаторы Комбинаторная логика, Алгоритмы Маркова, Трансформационные системы

                      

ФЯ

                                                                                                         

                                                                                       

                                                                                           

                                                                                           

Компиляция в коды абстрактных машин (АМ),SECD, KAM Комбинаторная логика, Категориальная комбинаторная логика(KKЛ).

                                                                                       

 

 

 

 

 

Расширенное λ-исчисление

λ (λ-абстракция);

@ (аппликация);

TRUE; FALSE; 0,1…; +; /; =; >; <; cons; head; tail (конструкторы данных);

null (распознает пустой список);

If … then… else…;

let;

letrec (позволяет явно записать подстановку); quote (возможно определение через K).

 (λx.x+3)3  let x=3 in x+3

 letrec fun =H(fun) in fun(arg)

Пример. a) let x=3 in λy.+xy→ λy.+3y

            b) Lisp       # '(lambda(x)                ML -fun foo [ ]=4 _{c о ns}

                                    (cоnd:                                   foo x=(x::3)

                                    (x(cons x’3))                        >val foo fn:(’а list)

                                    (# T ’ 4)))                                       →int list

JScript

function foo(x) {

if (x==null)                         // если список пуст,

         then new Array[x,3] //то результат- пара х,3

         else 4                   //,иначе 4

 

}

 

Расширенное λ - исчисление.

(λх(if x(@

      (@ cons x).

      (quote 3))

      (quote 4))                                   

cons ab →(a,b)

head (cons ab) →a

tail (cons ab) →b

 

Редукция графа

Любая программа может быть представлена ее синтаксическим деревом разбора.

Так как в “чистом” λ-исчислении всего две операции: λ и @, то будем в дальнейшем их использовать.

Пример. (λх.+х3)4

          1-ый способ                                                2-ой способ

                

      

 Здесь меняем все свободные вхождения х на 4

             

В качестве примера свернем это дерево разбора

    

Определение:

Аппликативный порядок редукции - такой порядок редукции, который предписывает свертывать самый левый из самых внутренних редексов.

Определение:

Нормальный порядок редукции - порядок редукции, который предписывает

свертывать самый левый из самых внешних редексов.

Пример. А: λх. If x≠ 0 then x else 3/Ø. Вычислим А от 4

                                (Это откровенная ошибка)      

                                              При аппликативном порядке редукции мы

                                    получим ошибку.

                                  При аппликативном порядке вычисляются

                                  все аргументы функции, а уже затем – сама функция.

                                  При нормальном порядке редукции аргументы

                                  вычисляются по мере надобности.

                                  При редуцировании графа мы будем пользоваться

                                  нормальным порядком редукции.

 

Алгоритм редукции графа (РГ)

Редукция графа будет осуществляться циклически.

Повторить:

Спускаемся по левой ветви графа до первой вершины, которая не является аппликацией, т.е. не помечена символом @.

Если эта вершина является корнем графа, то все выражение, находится в нормальной форме, значит окончание вычислений. Если она не является корнем, то она должна являться примитивной функцией либо аппликацией и у нее должны быть все необходимые аргументы (в противном случае ошибка). Мы рекурсивно применяем алгоритм для всех поддеревьев, являющихся аргументами.

Если текущая вершина является λ- вершиной, то рассматриваем следующие варианты:

1. она является корнем графа, значит выражение в нормальной форме.

2. если она не является корнем, то над ней может быть только аппликация @ и мы на место формального параметра λ-абстракции подставляем второе выражение из правой ветви аппликации. При необходимости это поддерево копируется.

Пример. (λх.+хх)7

 

(λху.+ху)3((λх.х)4)

 

 

Суперкомбинаторы.

  Определение:

Суперкомбинатором А арности n называется λ-выражение вида:

λх₁…х_n.Е, где на Е наложены следующие ограничения:

 λ-абстракция в Е является суперкомбинатором, Е не является λ-абстракцией,

А не содержит свободных переменных, при этом n≥0 (например, 3 (const) - это суперкомбинатор, арность n = 0).

 

Пример:

 3 - суперкомбинатор арности 0, Е=3

λху.+ху – суперкомбинатор арности 2

λх.+((λу.у)3)х n=1

λх.+(λу.+ху)3 не является суперкомбинатором, т.к. есть внутренняя λ-абстракция, которая содержит свободную переменную.

Вычислитель возьмет программу и начнет строить правила получения результата в виде супкркомбинаторов, далее будет он применять эти правила к аргументу.

Название суперкомбинаторов принято начинать со знака $.           

 λху.+ху

$Аab = +ab

Если этот суперкомбинатор применить к числам, то получается $A23, что также является суперкомбинатором.

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

Так как известно, что у суперкомбинаторов фиксированная арность, то вычислить, например, $A2 невозможно - не хватает аргументов.

              ┌──_↓^$B

λху.+ху=(λzу.+zу)x λх.+((λzу.+zy)x)3 теперь мы получили суперкомби-

                           ^↑───┘         └──_$Bx──┘

натор (все λ-абстракции, которые выражение содержит, являются суперкомбинаторами).

Переходы такого вида называются  введением экстра-параметра.

 

Алгоритм приведения λ-выражения к суперкомбинаторному виду

До тех пор пока в λ-выражении есть λ-абстракция. (Цикл While).

1.Выбирать λ-абстракцию, не содержащую других λ-абстракций (т.е. внутреннюю).

а) она является суперкомбинатором. Припишем ей некоторое имя и заменим ее вхождение этим именем.

б) не является суперкомбинатором, значит, содержит свободные переменные. Вынесем все свободные переменные в качестве экстра-параметров. Припишем получившейся λ-абстракции некоторое имя и заменим ее вхождение этим именем с соответствующими экстра-параметрами.

 

Пример.

λх.+((λу.+ху)3)х)4 = (λх.+((λz.λy +zy)x3)x)4 = { λz.λy.+zy=$A; $Aab=+ab} =

= (λх.+($Ax3)x)4 = {$Ba = +($Aa3)a} = $B4 = {$Prog=$B4} = $Prog

По λ-выражению получили набор суперкомбинаторов, по которому можем посчитать это выражение.

Определение.

Пусть $А - суперкомбинатор арности n, тогда его аппликация к n аргументам называется комбинаторным редексом.

Определение.

Суперкомбинатор арности 0 называется константной аппликативной формой.

Суперкомбинаторный редекс можно сворачивать, только если имеются все аргументы.

Пример. λху.-yх = λх.(λy-ух) = λх.+((λz.λy.-yz)x) = λх.$Yx = $X = $Y

                  $Yxy = -yx Устранение избыточных параметров.

                   $Xx = $Yx - эта строчка избыточная; по правилу (η) имеем:

                   $X = $Y  (η)- редукция (λх.Fx=F(x F))

 

Упорядочивание параметров.

Пусть имеется некоторое λ-выражение:

(…(λxz.+y(*xz))…)

Выносим у как экстра-параметр:

1-ый способ:                                                                                                _{↓подставляем у}

 λxz.+y(*xz) = λx.((λx.λу.λz.+y(*xz))xy) = λx.$Sxy = (λy.λx.$Sxy)y = $Ty

       ┌─────┐ _{Самая внутренняя λ-абстракция.}

   λx.[λz.+(*xz)]^.

 

 Обозначим $Sxyz = +y(*xz) (1)

                   λx.$Sxy - это не суперкомбинатор.

                  $Tyx = $Sxy (2)

                  $Ty - вычисляемое выражение.

2-ой способ:

λxz.+y(*xz) = (λy.λxz.+y(*xz)))y = λx.$yx = $Ty

$Syxz = +y(*xz)                   

Необходимо упорядочивать свободные переменные $Tyx = $Syx так, чтобы уже связанные переменные стояли последними в списке параметров.

 

$T = λy.λx.$Syx                  

$T = $S избыток.                           Возможность оптимизации суперкомбинатора.

λx.λу.+ху

               

 

х имеет глубину связывания 1 между х и его абстрагированием

у имеет глубину связывания 0 стоит 1 символ λ в дереве разбора   

 Сначала надо абстрагировать переменные  с минимальной глубиной связывания.

 Предполагается, что каждая переменная где-либо связана.