Выражение лямбда-исчисления

Question

Для лямбда-выражения (x (λx y. x y) z h) я не понял, как свободные переменные x (outer x), z и h могут быть преобразованы в коде C?

С уважением, дарк

Answer 1

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

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

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

Answer 2

Свободные переменные - это особый случай в лямбда-исчислении - их нельзя «преобразовать» во что-либо, поэтому обычно они воспринимаются как символы. В вашем примере, и учитывая некоторые фиктивные конструкторы для лямбда-выражений, вы бы перевели его на следующее (включая работу с неявным карри) C-подобным выражением:

mk_app(mk_app(mk_app(mk_sym("x"),
                     mk_lam("x",
                            mk_lam("y",
                                   mk_app(mk_var("x"),
                                          mk_var("y"))))),
              mk_sym("z")),
       mk_sym("h"));

Очевидно, что вы можете использовать mk_var() и для этих символов, но это может ввести в заблуждение, поскольку они на самом деле не являются переменными, поскольку они не связаны. Другими словами, если вы выполните какое-либо альфа-преобразование в выражении, они должны остаться прежними.

(Кстати, соответствующая часть здесь - допущение Барендрегта о свободной переменной.)