В лямбда-исчислении, что если применить выражение к нефункциональному выражению?

Question

Я новичок в Lambda Calculus. Я читал об определении лямбда-выражения в Википедии.

Множество лямбда-выражений, Λ, может быть определено индуктивно:

1. Если x переменная, то x ∈ Λ
2. Если x переменная и M ∈ Λ, то (λx.M) ∈ Λ
3. Если M, N ∈ Λ, то (M N) ∈ Λ

Экземпляры правила 2 называются абстракциями, а экземпляры правила 3 ​​- приложениями.

Я знаю значение правила 2, когда M - это абстракция функции, то есть в форме (λx.E).

Но какой смысл, когда М не является функцией? Например, просто переменная x или нефункциональное выражение x + y

Answer 1

Лямбда-исчисление состоит из контекстно-свободной грамматики

E ::= v        Variable
   |  λ v. E   Abstraction
   |  E E      Application

где v диапазоны по переменным, вместе с правилами бета- и эта-редукции

(λ x. B) E  ->  B   where every occurrence of x in B in substituted by E
  λ x. E x  ->  E   if x doesn't occur free in E

a свободен в λ b. b a, но не в λ a. λ b. b a, Выражение, к которому не применимо ни одно из двух правил сокращения, находится в нормальной форме.

Так что если M N это не бета-редекс (λ x. B) Eи оба M а также N в нормальной форме, то M N целое находится в неприводимой нормальной форме.

Answer 2

Итак, значение (M N) вам ясно, когда M - функция. Для простоты рассмотрим случай тождества, т. Е. M = I = \xx

                          (*)    (\x.x) N 

это сводится к N. Предположим, теперь вы хотите сделать свою программу более общей. Вы не хотите просто применять тождество к N, но применять универсальную функцию f, которую вы берете в качестве ввода. Итак, вы заменяете \ xx на f и абстрагируете весь термин от f:

                                 \f.f N

это следует понимать как \f.(f N). Довольно просто

Теперь вы можете передать идентификатор в качестве аргумента к предыдущему термину, чтобы получить термин, эквивалентный (*):

                       (\f.f N) \x.x = \x.x N

Чтобы сделать вещи еще более сложными, вы можете представить, что обработаете свою входную функцию f, прежде чем применять ее к N. Например, если вы ожидаете двоичную (криптованную) функцию в качестве входного, вы можете применить f к "паре" аргументов. (N,N), что, так как f прокручивается, равняется передаче N в качестве аргумента дважды:

                        (**)    \f. f N N

следует понимать как \f. ((Ф Н) Н). Итак, вы ясно видите смысл наличия приложений в функциональном положении других приложений.

Чтобы увидеть предыдущий пример на работе, возьмите термин K = \x.\ Yx вместо тождества. K ест два аргумента и возвращает первый. Если вы введете K в качестве входных данных для предыдущего термина, вы все равно получите термин, эквивалентный (*)

                       (\f.f N N) K = K N N = N

В общем, языки программирования - это способ предоставления абстракций. Чтобы абстрагироваться по отношению к понятию, вам прежде всего нужен способ дать имя экземплярам понятия. Например, в императивном языке переменная по сути является абстракцией ячейки памяти. Чтобы абстрагироваться от функций, вам нужна возможность использовать имена для функций. Второй шаг, это позволить понятиям быть "выразимыми", то есть предоставить язык выражений, который позволяет динамически синтезировать новые экземпляры данного понятия (в нашем случае, новые функции). Лямбда-исчисление - это просто базовое исчисление, в котором функции (непосредственно) выразимы.