Список свободных переменных лямбда-выражения

Question

Я просто делал домашнюю работу для моего предстоящего теста OCaml, и у меня возникли некоторые проблемы.

Рассмотрим язык λ-терминов, определенных следующим абстрактным синтаксисом (где x - переменная):

t ::= x | t t | λx. t  

Напишите типовой термин для представления λ-терминов. Предположим, что переменные представлены в виде строк.

Хорошо мальчик

# type t = Var of string | App of (t*t) | Abs of string*t;;
type t = Var of string | App of (t * t) | Abs of (string * t)

Свободные переменные fv(t) члена t определяются индуктивно следующим образом:

fv(x) = {x}  
fv(t t') = fv(t) ∪ fv(t')  
fv(λx. t) = fv(t) \ {x}

Конечно, вещь.

# let rec fv term = match term with
Var x -> [x]
  | App (t, t') -> (List.filter (fun y -> not (List.mem y (fv t'))) (fv t)) @ (fv t')
  | Abs (s, t') -> List.filter (fun y -> y<>s) (fv t');;
      val fv : t -> string list = <fun>

Например,

fv((λx.(x (λz.y z))) x) = {x,y}.

Давайте проверим это.

# fv (App(Abs ("x", App (Abs ("z", Var "y"), Var "z")), Var "x"));;
- : string list = ["y"; "z"; "x"]

Я проверил миллион раз, и я уверен, что результат должен включать переменную "z". Можете ли вы меня успокоить?

Answer 1

В комментариях к ОП указывалось на вид @PasqualCuoq, который λ в лямбда-исчислении ассоциируется так же, как fun в OCaml. То есть термин t in λx.t оценивается жадно (см. http://en.wikipedia.org/wiki/Lambda_calculus).

Это значит, что (λz.y z) на самом деле (λz.(y z))и что приведенная выше функция верна, но для примера выражения приведен перевод (λx.(x (λz.y z))) x не так, как должно было быть

(App(Abs("x", App(Var "x", Abs("z", App(Var "y", Var "z")))), Var "x"))

на месте

(App(Abs ("x", App (Abs ("z", Var "y"), Var "z")), Var "x"))

Вот это удивительное место под названием Stack Overflow!