Lambda calculus implementation using CBV small step operational semantics

Question

I'm trying to implement an interpreter for the lambda calculus that has constant intergers and supports the addition operation. The interpreter should use the call-by-value small-step operational semantics. So I've implemented a step that should be able to reduce a lambda term by one step. However, the stepper is losing the surrounding program of the reduced subterm when reduced.

This is my implementation in 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

and the stepper looks like this:

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)

So, given the following example of a program (\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)))

I expect the step function to only reduce the 21 + 21 while keeping the rest of the program i.e. I expect the following output after one step (\x.(\y.y x) 42) \x.x + 1. However, I'm not able to retain the surrounding code around the Cst 42. How should I modify the program such that it reduction only steps once while maintaining the rest of the program?

You call step recursively and this is, why it is "multistep", yes? And the recursion ends when it hits something "terminal" i.e. non-recursive. If you really only want 1 operation at a time, I think the "standard" option is to rewrite this function in a non-recursive style first. This typically involves some form of manual stack with the "leftovers" after 1 step. `step env exp -> (env,exp)` — BitTickler, Dec 07 '22 at 18:44
Can you elaborate on this? I believe the recursive call is necessary to resolve eventual bindings and environment updates. — Winston Smith, Dec 07 '22 at 19:40
https://stackoverflow.com/questions/4422032/rewriting-a-recursive-function-without-using-recursion — BitTickler, Dec 07 '22 at 19:42

score 1 · Accepted Answer · answered Dec 07 '22 at 19:59

I think there are two things that you should do differently if you want to implement standard small-step CBV lambda calculus.

First, you want to always perform just one step. This means that you should always call step recursively only once. For example, you have Arith(Plus, step a env, step b env) - but this means that if you have an expression representing (1+2)+(2+3), you will reduce this in "one step" to 3+5 but this is really two steps in one.
Second, I don't think your way of handling variables will work. If you have (\x.x+2) 1, this should reduce to 1+2 using variable substitution. You could reduce this to x+2 and remember the assignment x=1 on the side, but then your function would need to work on expression alongside with variable assignment Exp * Map<string, Exp> -> Exp * Map<string, Exp>. It is easier to use normal substitution, at least for the start.

So, I would first define subst x repl exp which substitutes all free occurences of x in the expression exp with 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)

Now you can implement your step function.

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)

Using your example:

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

I get:

App (Cst 42, Abs ("x", Arith (Plus, Var "x", Cst 1)))

And if I'm correctly making sense of your example, this is correct - because now you are trying to treat a number as a function, which gets stuck.

Lambda calculus implementation using CBV small step operational semantics

1 Answers1