Я пытаюсь реализовать интерпретатор лямбда-исчисления, который имеет постоянные числа и поддерживает операцию сложения. Интерпретатор должен использовать операционную семантику вызова по значению с малым шагом. Поэтому я реализовал step
, который должен уменьшить лямбда-член на один шаг. Однако при сокращении степпер теряет окружающую программу сокращенного подтерма.
Это моя реализация на F#:
type Exp =
| Cst of int
| Var of string
| Abs of string * Exp
| App of Exp * Exp
| Arith of Oper * Exp * Exp
and Oper =
Plus
и степпер выглядит так:
let rec step (exp : Exp) (env : Map<string, Exp>) : Exp =
match exp with
| Cst _ | Abs(_) -> exp
| Var x ->
match Map.tryFind x env with
| Some v -> v
| None -> failwith "Unbound variable"
| App(e1, e2) ->
match step e1 env with
| Abs(x, e) ->
let newEnv = Map.add x (step e2 env) env
step e newEnv
| e1' -> failwithf "%A is not a lambda abstraction" e1'
| Arith(Plus, Cst a, Cst b) -> Cst (a + b)
| Arith(Plus, e1, Cst b) -> Arith(Plus, step e1 env, Cst b)
| Arith(Plus, Cst a, e2) -> Arith(Plus, Cst a, step e2 env)
| Arith(Plus, a, b) -> Arith(Plus, step a env, step b env)
Итак, учитывая следующий пример программы (\x.(\y.y x) 21 + 21) \x.x + 1
App
(Abs
("x", App (Abs ("y", App (Var "y", Var "x")), Arith (Plus, Cst 21, Cst 21))),
Abs ("x", Arith (Plus, Var "x", Cst 1)))
Я ожидаю, что функция step
уменьшит только 21 + 21
, сохранив при этом остальную часть программы, то есть я ожидаю следующий результат после одного шага (\x.(\y.y x) 42) \x.x + 1
. Однако я не могу сохранить окружающий код вокруг Cst 42
. Как мне изменить программу так, чтобы она сокращала только один шаг, сохраняя при этом остальную часть программы?
Вы можете остановиться на этом? Я считаю, что рекурсивный вызов необходим для разрешения возможных привязок и обновлений среды.
Я думаю, что есть две вещи, которые вы должны сделать по-другому, если хотите реализовать стандартное лямбда-исчисление CBV с малым шагом.
Во-первых, вы хотите всегда выполнять только один шаг. Это означает, что вы всегда должны вызывать step
рекурсивно только один раз. Например, у вас есть Arith(Plus, step a env, step b env)
, но это означает, что если у вас есть выражение, представляющее (1+2)+(2+3)
, вы уменьшите его за «один шаг» до 3+5
, но на самом деле это два шага за один.
Во-вторых, я не думаю, что ваш способ обработки переменных будет работать. Если у вас есть (\x.x+2) 1
, это должно уменьшиться до 1+2
с помощью подстановки переменных. Вы можете сократить это до x+2
и запомнить присваивание x=1
сбоку, но тогда ваша функция должна будет работать с выражением вместе с присваиванием переменной Exp * Map<string, Exp> -> Exp * Map<string, Exp>
. Легче использовать обычную замену, по крайней мере, для начала.
Итак, я бы сначала определил subst x repl exp
, который заменяет все свободные вхождения x
в выражении exp
на repl
:
let rec subst (n : string) (repl : Exp) (exp : Exp) =
match exp with
| Var x when x = n -> repl
| Cst _ | Var _ -> exp
| Abs(x, _) when x = n -> exp
| Abs(x, b) -> Abs(x, subst n repl b)
| App(e1, e2) -> App(subst n repl e1, subst n repl e2)
| Arith(op, e1, e2) -> Arith(op, subst n repl e1, subst n repl e2)
Теперь вы можете реализовать свою функцию step
.
let rec step (exp : Exp) =
match exp with
// Values - do nothing & return
| Cst _ | Abs _ -> exp
// There should be no variables, because we substituted them
| Var x -> failwith "Unbound variable"
// App #1 - e1 is function, e2 is a value, apply
| App(Abs(x, e1), (Cst _ | Abs _)) -> subst x e2 e1
// App #2 - e1 is not a value, reduce that first
| App(e1, e2) -> App(step e1, e2)
// App #3 - e1 is value, but e2 not, reduce that
| App(Abs(x,e1), e2) -> App(Abs(x,e1), step e2)
// Similar to App - if e1 or e2 is not value, reduce e1 then e2
| Arith(Plus, Cst a, Cst b) -> Cst (a + b)
| Arith(Plus, Cst a, e2) -> Arith(Plus, Cst a, step e2)
| Arith(Plus, a, b) -> Arith(Plus, step a, b)
Используя ваш пример:
App
(Abs
("x", App (Abs ("y", App (Var "y", Var "x")), Arith (Plus, Cst 21, Cst 21))),
Abs ("x", Arith (Plus, Var "x", Cst 1)))
|> step
|> step
|> step
|> step
Я получил:
App (Cst 42, Abs ("x", Arith (Plus, Var "x", Cst 1)))
И если я правильно понимаю ваш пример, это правильно, потому что теперь вы пытаетесь рассматривать число как функцию, которая застревает.
Вы называете шаг рекурсивно, и вот почему он «многошаговый», да? И рекурсия заканчивается, когда она сталкивается с чем-то «терминальным», то есть нерекурсивным. Если вам действительно нужна только одна операция за раз, я думаю, что «стандартный» вариант - сначала переписать эту функцию в нерекурсивном стиле. Обычно это включает некоторую форму ручного стека с «остатками» после 1 шага.
step env exp -> (env,exp)