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

Я просто делал домашнее задание для моего предстоящего теста 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". Не могли бы вы меня в этом успокоить?


ocaml lambda-calculus free-variable
person rickmeizter    schedule 09.12.2012    source источник
comment
Нет, z не является свободной переменной (λz.y z) и, следовательно, не является свободной переменной (λx.(x (λz.y z))) x.   -  person Pascal Cuoq    schedule 09.12.2012
comment
Я все еще ломаю голову над тем, почему ваш код вычисляет неправильный ответ, но List.filter (fun y -> not (List.mem y (fv t'))) (fv t), хотя он пока кажется мне правильным, вычисляет fv t' много раз. Вы должны вычислить его один раз с помощью let fv_t' = fv t' in … и использовать fv_t'.   -  person Pascal Cuoq    schedule 09.12.2012
comment
@PascalCuoq Думаю, я понял. Я читал (λz.y z) как ((λz.y) z), хотя на самом деле это должно читаться как (λz.(y z)). Дело в том, что ничто не указывало мне на такую ​​ассоциацию. Спасибо и за совет по оптимизации!   -  person rickmeizter    schedule 09.12.2012
comment
Да, λ в лямбда-исчислении ассоциируется с тем же, что и fun в OCaml. Выражение fun x -> st uff совпадает с fun x -> (st uff).   -  person Pascal Cuoq    schedule 09.12.2012
comment
Должны ли мы оставить вопрос?   -  person rickmeizter    schedule 09.12.2012
comment
Ну, я помню, как весь класс был в замешательстве, пока один из нас не понял, что «λ был таким же, как fun в Caml», так что это правильный вопрос. Вместо того, чтобы удалять вопрос, вы должны записать свое открытие в качестве ответа и принять его.   -  person Pascal Cuoq    schedule 09.12.2012
comment
Очень хорошо, еще раз спасибо!   -  person rickmeizter    schedule 09.12.2012

Ответы (1)


arrow_upward
3
arrow_downward

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

Это означает, что (λ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!

person rickmeizter    schedule 09.12.2012