README.md

    ИНТЕРПРЕТАТОР ВЫРАЖЕНИЙ ЛЯМБДА ИСЧИСЛЕНИЯ

    Данный проект реализует интерпретатор выражений лямбда исчисления, задаваемых в синтаксисе ЛИСП. Предназначен для экспериментов с лямбда выраженями, для улучшения понимания их работы, с этой целью каждое вычисление редукции сопровождается подробной печатью выполненых действий. Эта печать управляется с помощью глобальных флагов, я рекомендую установить их так:

    (set! betta-reduction-in-prn  #f)
    (set! betta-reduction-out-prn #f)
    (set! delta-reduction-in-prn  #f)
    (set! delta-reduction-out-prn #f)
    (set! full-expression-prn     #t)
    

    тогда после каждой редукции будет печататься полное выражение полученное после очередного шага редукции.

    Очень простой интерпретатор использующий бетта и дельта редукции(так было в начале, но из за “захвата” переменных и их значений в выражениях, интерпретатор пришлось “немного” усложнить). В основе дельта редукции лежит функция замены переменных значениями tree-expr-replace, которая проходит по дереву выражения и заменяет все вхождения переменных, за исключением лямбда функций определения которых “затеняют” данный символ. В последней версии я реализовал ещё замену имён переменных в лямбда выражении, если при редукции происходит “захват” переменной, это что то вроде альфа-редукции.

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

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

    (predefined-add 'K '(lambda (a b) a))
    (find-predefined 'SQUARE)
    (predefined-del 'SQUARE)
    
    

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

    (define t2 '((lambda (x) (- (* x (+ 4 x 2) ((lambda (x) (+ x 13 (- x 2))) 140)) x)) 15))
    (meval t2)
    ->{- {* 15 {+ 4 15 2} {{lambda {x} {+ x 13 {- x 2}}} 140}} 15}
    ->{- {* 15 21 {{lambda {x} {+ x 13 {- x 2}}} 140}} 15}
    ->{- {* 15 21 {+ 140 13 {- 140 2}}} 15}
    ->{- {* 15 21 {+ 140 13 138}} 15}
    ->{- {* 15 21 291} 15}
    ->{- 91665 15}
    ->91650
    91650
    

    Лямбда выражения, передаваемые интерпретатору(функции meval), представляют собой обычные списки. Выражения-списки состоят из определений лямбда функций, базовых-примитивных процедур или символов из списка предопределённых лямбда функций.

    Редуцирование рекурсивных выражений:

    (define SUM1 '(lambda (s)
                     (lambda (n)
                        (if (= n 0) 0 (+ n (s (- n 1)))))))
    
    (meval `((Y ,SUM1) 3))
    ->{{{lambda {x}
          {{lambda {s} {lambda {n} {if {= n 0} 0 {+ n {s {- n 1}}}}}}
           {lambda {y} {{x x} y}}}}
        {lambda {x}
          {{lambda {s} {lambda {n} {if {= n 0} 0 {+ n {s {- n 1}}}}}}
           {lambda {y} {{x x} y}}}}}
       3}
    ->{{{lambda {s} {lambda {n} {if {= n 0} 0 {+ n {s {- n 1}}}}}}
        {lambda {y}
          {{{lambda {x}
              {{lambda {s} {lambda {n} {if {= n 0} 0 {+ n {s {- n 1}}}}}}
               {lambda {y} {{x x} y}}}}
            {lambda {x}
              {{lambda {s} {lambda {n} {if {= n 0} 0 {+ n {s {- n 1}}}}}}
               {lambda {y} {{x x} y}}}}}
           y}}}
       3}
    ->{{lambda {n}
         {if {= n 0}
           0
           {+
            n
            {{lambda {y}
               {{{lambda {x}
                   {{lambda {s} {lambda {n} {if {= n 0} 0 {+ n {s {- n 1}}}}}}
                    {lambda {y} {{x x} y}}}}
                 {lambda {x}
                   {{lambda {s} {lambda {n} {if {= n 0} 0 {+ n {s {- n 1}}}}}}
                    {lambda {y} {{x x} y}}}}}
                y}}
             {- n 1}}}}}
       3}
    
    ..... очень много строк.
    
    
    ->{+
       3
       {+
        2
        {+
         1
         {{= {- 1 1} 0}
          0
          {+
           {- {- {- 3 1} 1} 1}
           {{lambda {y}
              {{{lambda {x}
                  {{lambda {s} {lambda {n} {if {= n 0} 0 {+ n {s {- n 1}}}}}}
                   {lambda {y} {{x x} y}}}}
                {lambda {x}
                  {{lambda {s} {lambda {n} {if {= n 0} 0 {+ n {s {- n 1}}}}}}
                   {lambda {y} {{x x} y}}}}}
               y}}
            {- {- {- {- 3 1} 1} 1} 1}}}}}}}
    ->{+
       3
       {+
        2
        {+
         1
         {{= 0 0}
          0
          {+
           {- {- {- 3 1} 1} 1}
           {{lambda {y}
              {{{lambda {x}
                  {{lambda {s} {lambda {n} {if {= n 0} 0 {+ n {s {- n 1}}}}}}
                   {lambda {y} {{x x} y}}}}
                {lambda {x}
                  {{lambda {s} {lambda {n} {if {= n 0} 0 {+ n {s {- n 1}}}}}}
                   {lambda {y} {{x x} y}}}}}
               y}}
            {- {- {- {- 3 1} 1} 1} 1}}}}}}}
    ->{+
       3
       {+
        2
        {+
         1
         {true
          0
          {+
           {- {- {- 3 1} 1} 1}
           {{lambda {y}
              {{{lambda {x}
                  {{lambda {s} {lambda {n} {if {= n 0} 0 {+ n {s {- n 1}}}}}}
                   {lambda {y} {{x x} y}}}}
                {lambda {x}
                  {{lambda {s} {lambda {n} {if {= n 0} 0 {+ n {s {- n 1}}}}}}
                   {lambda {y} {{x x} y}}}}}
               y}}
            {- {- {- {- 3 1} 1} 1} 1}}}}}}}
    ->{+ 3 {+ 2 {+ 1 0}}}
    ->{+ 3 {+ 2 1}}
    ->{+ 3 3}
    ->6
    6
    
    

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

    Примитивные процедуры работающие со списками: car, cdr, cons, list, list-ref, set-car!, set-cdr!, null?, member на самом деле работают с частями входного выражения. Хотя если эти выражения не содержат определений лямбда выражений, они вполне себе могут эмулировать работу со списками.

    Примитивная функция make-lambda и синтаксис quote, не являются необходимым для работы с лямбда выражениями, а реализован как его расширение, для построения конструкций, типа макросов. Дело в том что при реалзиации конструкции letvar я столкнулся с невозможностью замены имён параметров в уже имеющихся записях лямбда функций, поэтому была реалзована make-lambda обходящая данный запрет. Думаю они могут послужить некой надстройкой над языком лямбда выражений, позволяющей писать более гибкий код.

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

    
    > ft13
    '(lambda (T)
       (tuple
        (lambda (s) (lambda (n) (if (= n 0) 0 ((INDEX-T T 2) n))))
        (lambda (s) (lambda (n) (+ n ((INDEX-T T 1) (- n 1)))))))
    
    
    > `((INDEX-T ,ft13 1) 5)
    '((INDEX-T
       (lambda (T)
         (tuple
          (lambda (s) (lambda (n) (if (= n 0) 0 ((INDEX-T T 2) n))))
          (lambda (s) (lambda (n) (+ n ((INDEX-T T 1) (- n 1)))))))
       1)
      5)
    
    
    > (predefined-expand `((INDEX-T ,ft13 1) 5))
    '(((lambda (x i)
         ((lambda (f)
            ((lambda (x) (f (lambda (y) ((x x) y))))
             (lambda (x) (f (lambda (y) ((x x) y))))))
          (list-ref (x x) i)))
       (lambda (T)
         (tuple
          (lambda (s)
            (lambda (n)
              ((lambda (p q r) (p q r))
               (= n 0)
               0
               (((lambda (x i)
                   ((lambda (f)
                      ((lambda (x) (f (lambda (y) ((x x) y))))
                       (lambda (x) (f (lambda (y) ((x x) y))))))
                    (list-ref (x x) i)))
                 T
                 2)
                n))))
          (lambda (s)
            (lambda (n)
              (+
               n
               (((lambda (x i)
                   ((lambda (f)
                      ((lambda (x) (f (lambda (y) ((x x) y))))
                       (lambda (x) (f (lambda (y) ((x x) y))))))
                    (list-ref (x x) i)))
                 T
                 1)
                (- n 1)))))))
       1)
      5)
    
    

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

    Я попытался поэксперементировать с комбинаторами из теории комбинаторной логики, некоторые примеры заработали, но выяснилось, что при попытке погрузить комбинаторы из комбинаторной логики в лямбда исчисление возникает ряд проблем. В частности в комбинаторной логике очень “легкомысленно” относятся к передаваемым в функцию-комбинатор параметрам. Т.е. в ней часто неважно сколько параметров передано в функцию, считается что функции от этого хуже не будет. Поэтому возникают, так называемые частичные применения. Т.е в функцию 3х аргументов можно передать два аргумента, и она вместо ошибки пременения, должна вернуть функцию ждущую один аргумент. Не говоря уже о так называемом - каррировании, приводящем все все функции выражения к набору одноаргументных функций. Что касается, частичного примениния, я реализовал это в интерперетаторе.

    ;;частичное применение
    
    (meval '(+)) ;
    (meval '(+ 1)) ; |+745|
    
    (meval '((+ 1) 2 3)) ;
    WARNING: partial apply primitive func, need 2 args, actualy: 1
    ->{+692 2 3}
    ->6
    6
    

    где “+692” это имя сгенерированной функции + 1 применяемой к аргументам 2 и 3. Работа с частичными применениями ещё “немного” запутала логику интерперетатора.

    Описание

    interpreter lambda expression

    Конвейеры
    0 успешных
    0 с ошибкой