(Interpreter, deBruijin style) Termination checker

Stream: lean4

[McCoy R. Becker]

Hi all! New to the community. I've been playing around with Lean 4 for a bit. I'm trying to write an applicative order evaluation interpreter for a lambda calculus with natural numbers, and binary primitives (addition, etc).

I wrote a deBrujin style eval for this, but I'm hitting the termination checker. I dumped my interpreter into a file: https://github.com/femtomc/logical_relations.lean/blob/main/IntroLogicalRelations.lean

Lean tells me that the issue is here: https://github.com/femtomc/logical_relations.lean/blob/c99b4604b9e1acde704db896efae0171ee25666f/IntroLogicalRelations.lean#L38 -- in LAbs, I shift the environment and extend it before evaluating the shadowed term t.

I think this extension upsets proving termination, but I'm not exactly sure how to remedy it.

[Joachim Breitner]

Hi and welcome!

Unrelated note: your github repository contains the .lake file; it is usually not added to the repository.

I had to add import Mathlib to the file to be able to load it.

[McCoy R. Becker]

thanks for these tips! Will adapt my code to this

[Joachim Breitner]

The error message mentions termination_by, and if you think your function is recursing on the size of the term, you can add

termination_by eval env t => t

after the function. But then the recursive call eval env (subst 0 v_eval t) complains.

At this point, maybe step back and ponder if eval really _is_ terminating, or not. It’s an evaluator for lambda terms, so probably not… in which case, def eval won’t work like this.

Maybe others have good domain-specific advise for what to do instead :-)

[Mario Carneiro]

Well the obvious solution is to use partial def eval instead

[McCoy R. Becker]

Interesting, thanks for the suggestion -- I'll explore it.

I'm trying to understand if (a) I've messed up the interpreter, or (b) it is written correctly, but I need to use well-founded recursion or (c) if partial def will work for my needs.

[Mario Carneiro]

An interpreter for lambda calculus is not terminating

[Mario Carneiro]

so yes this is written correctly and you should not expect to be able to prove termination

[Mario Carneiro]

As for whether partial def will work for your needs, that depends on what you want to do with this definition. If you just want to run it using #eval or compile it then yes this will work fine. If you want to prove properties about this function then no it won't work, because partial defs are opaque, you can't prove anything about them beyond their type. If you want to have both runnable code and something you can prove properties about it will be somewhat more complicated, you will need some predicate asserting that the input terminates, or alternatively you can use a fuel variable to make the definition "time out" after running for a while (and therefore make it terminating by fiat)

[Joachim Breitner]

partial def eval means you can run the interpreter, but not prove anything about it – depends on what… whatever Mario says :-)

[McCoy R. Becker]

I'm interesting in proving things. Fuel makes sense here.

[McCoy R. Becker]

Thanks for the ideas!

[McCoy R. Becker]

This _seems_ better, but still doesn't pass:

def eval : ℕ -> Env → Term → Term
| 0, _, t@(_) => t
| fuel, env, Term.Nat n => Term.Nat n
| fuel, env, Term.Var n => (lookupEnv env n).getD (Term.Var n)
| fuel, env, Term.Abs t => Term.Abs (eval (fuel - 1) (Term.Var 0 :: env.map (shift 1)) t)
| fuel, env, Term.Prim f => Term.Prim f
| fuel, env, (Term.App (Term.Abs t) v) =>
  let v_eval := eval (fuel - 1) env v;
  eval (fuel - 1) env (subst 0 v_eval t)
| fuel, env, (Term.App t1 t2) =>
  let t1_eval := eval (fuel - 1) env t1;
  let t2_eval := eval (fuel - 1) env t2;
  eval (fuel - 1) env (Term.App t1_eval t2_eval)

termination_by eval fuel env t => fuel

Perhaps I'm not using the match guard / check correctly?

[Mario Carneiro]

use fuel+1 on the left rather than fuel-1 on the right

[Mario Carneiro]

def eval : ℕ -> Env → Term → Term
| 0, _, t@(_) => t
| fuel+1, env, Term.Nat n => Term.Nat n
| fuel+1, env, Term.Var n => (lookupEnv env n).getD (Term.Var n)
| fuel+1, env, Term.Abs t => Term.Abs (eval fuel (Term.Var 0 :: env.map (shift 1)) t)
| fuel+1, env, Term.Prim f => Term.Prim f
| fuel+1, env, (Term.App (Term.Abs t) v) =>
  let v_eval := eval fuel env v;
  eval fuel env (subst 0 v_eval t)
| fuel+1, env, (Term.App t1 t2) =>
  let t1_eval := eval fuel env t1;
  let t2_eval := eval fuel env t2;
  eval fuel env (Term.App t1_eval t2_eval)

[Mario Carneiro]

no need for termination_by either

[McCoy R. Becker]

huh, that's interesting -- any intuition?

[Mario Carneiro]

This is a definition by structural recursion on Nat, so you want to use the constructors of Nat which are 0 and n+1

[Mario Carneiro]

besides this, fuel - 1 is not necessarily smaller than fuel because 0 - 1 = 0

[McCoy R. Becker]

Ah, great explanation, thank you

[Mario Carneiro]

You have a 0 case, but the typechecker doesn't know that