Реализация лямбда-исчисления с использованием операционной семантики малого шага CBV

Я пытаюсь реализовать интерпретатор лямбда-исчисления, который имеет постоянные числа и поддерживает операцию сложения. Интерпретатор должен использовать операционную семантику вызова по значению с малым шагом. Поэтому я реализовал 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. Как мне изменить программу так, чтобы она сокращала только один шаг, сохраняя при этом остальную часть программы?

Вы называете шаг рекурсивно, и вот почему он «многошаговый», да? И рекурсия заканчивается, когда она сталкивается с чем-то «терминальным», то есть нерекурсивным. Если вам действительно нужна только одна операция за раз, я думаю, что «стандартный» вариант - сначала переписать эту функцию в нерекурсивном стиле. Обычно это включает некоторую форму ручного стека с «остатками» после 1 шага. step env exp -> (env,exp)

BitTickler 07.12.2022 19:44

Вы можете остановиться на этом? Я считаю, что рекурсивный вызов необходим для разрешения возможных привязок и обновлений среды.

Winston Smith 07.12.2022 20:40
stackoverflow.com/questions/4422032/…
BitTickler 07.12.2022 20:42
Введение в одну из самых важных концепций в React - функциональное программирование
Введение в одну из самых важных концепций в React - функциональное программирование
React разработан с использованием концепции функционального программирования, поэтому понимание функционального программирования важно для изучения...
Фото ️🔁 Radek Jedynak 🔃 on ️🔁 Unsplash 🔃
Фото ️🔁 Radek Jedynak 🔃 on ️🔁 Unsplash 🔃
Что такое Java 8 Streams API? Java 8 Stream API
1
3
54
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

Я думаю, что есть две вещи, которые вы должны сделать по-другому, если хотите реализовать стандартное лямбда-исчисление 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)))

И если я правильно понимаю ваш пример, это правильно, потому что теперь вы пытаетесь рассматривать число как функцию, которая застревает.

Другие вопросы по теме