Lambda-Pi (λπ) to Lean Translation Plan

Overview

Translate the λπ (lambda-py) Python semantics from Racket/PLT Redex to Lean 4, using:

Small-step semantics (faithful to Redex reduction relation)
Core subset first (incrementally expand)
Mathlib for maps, sets, and proof infrastructure

Source Analysis Summary

The λπ semantics (in lambda-py/redex/) models Python with:

State Structure

(e, ε, Σ) where:
  e = expression being evaluated
  ε = environment (variable name → heap reference)
  Σ = store/heap (reference → value)

Core Constructs

Category	Constructs
Memory	`ref`, `fetch`, `set!`, `alloc`
Control	`if`, `seq`, `while`, `break`, `continue`
Functions	`fun`, `app`, `frame`, `return`
Variables	`id x t` (with global/local scope)
Objects	`object`, `get-attr`, `set-attr`
Exceptions	`raise`, `tryexcept`, `tryfinally`, `err`

Meta-values (Python object internals)

meta-num, meta-str, meta-none
meta-list, meta-tuple, meta-set
meta-closure, meta-code, meta-class

Lean Module Structure

PythonOfLean/
├── Syntax/
│   ├── Expr.lean         -- Expression inductive type
│   ├── Value.lean        -- Values, MetaVal, ObjVal
│   └── Primitive.lean    -- Primitive operation names
├── Semantics/
│   ├── Store.lean        -- Store type and operations
│   ├── Env.lean          -- Environment type and operations
│   ├── State.lean        -- Combined program state
│   ├── Subst.lean        -- Capture-avoiding substitution
│   ├── Step.lean         -- Small-step reduction relation
│   └── Eval.lean         -- Multi-step evaluation (reflexive-transitive closure)
├── Primitives/
│   └── Delta.lean        -- δ function for primitive operations
└── Examples/
    └── Basic.lean        -- Example programs and tests

Core Type Definitions

References and Names

-- Heap references (natural numbers as addresses)
abbrev Ref := Nat

-- Variable names
abbrev VarName := String

-- Scope classification (critical for Python semantics)
inductive ScopeType where
  | global   -- Looked up in environment ε
  | local    -- Substituted directly (becomes Ref)
  deriving DecidableEq, Repr, BEq

Meta-Values

/-- Internal representation of Python values -/
inductive MetaVal where
  | none                                    -- Python None
  | num (n : Int)                           -- Numbers
  | str (s : String)                        -- Strings
  | list (vs : List Ref)                    -- List of references
  | tuple (vs : List Ref)                   -- Tuple of references
  | set (vs : List Ref)                     -- Set of references
  | closure (params : List VarName)         -- Function closure
            (vararg : Option VarName)       -- Optional *args
            (body : Expr)
  | code (params : List VarName)            -- Code object
         (kwarg : VarName)
         (body : Expr)
  | class_ (name : VarName)                 -- Class reference
  deriving Repr

Values

/-- Runtime values -/
inductive Val where
  | pointer (r : Ref)                       -- Heap reference
  | sym (s : String)                        -- String symbol
  deriving Repr, BEq, DecidableEq

/-- Object value with class, meta-value, and field dictionary -/
structure ObjVal where
  cls : Val                                 -- Class pointer
  meta : MetaVal                            -- Internal data
  fields : List (String × Ref)              -- Field name → ref
  deriving Repr

Expressions

/-- Core λπ expressions -/
inductive Expr where
  -- Values and references
  | val (v : Val)
  | objVal (o : ObjVal)
  | ref (r : Ref)
  | undefined

  -- Variables
  | id (x : VarName) (t : ScopeType)
  | letIn (x : VarName) (t : ScopeType) (bound : Expr) (body : Expr)
  | assign (lhs : Expr) (rhs : Expr)
  | delete (e : Expr)

  -- Memory operations
  | alloc (e : Expr)
  | fetch (e : Expr)
  | set! (loc : Expr) (val : Expr)

  -- Control flow
  | seq (e1 e2 : Expr)
  | ifThenElse (cond then_ else_ : Expr)
  | while (cond body else_ : Expr)
  | loop (body next : Expr)
  | break
  | continue

  -- Functions
  | fun_ (params : List VarName) (vararg : Option VarName) (body : Expr)
  | app (fn : Expr) (args : List Expr)
  | frame (e : Expr)
  | return_ (e : Expr)

  -- Objects
  | object (cls : Expr) (meta : MetaVal)
  | getAttr (obj attr : Expr)
  | setAttr (obj attr val : Expr)

  -- Collections (convenience forms that allocate)
  | list (cls : Expr) (elems : List Expr)
  | tuple (cls : Expr) (elems : List Expr)
  | set_ (cls : Expr) (elems : List Expr)

  -- Exceptions
  | raise (e : Expr)
  | err (v : Val)
  | tryExcept (try_ : Expr) (x : VarName) (catch_ else_ : Expr)
  | tryFinally (try_ finally_ : Expr)

  -- Primitives
  | builtinPrim (op : String) (args : List Expr)

  -- Modules (defer for later)
  | module (e1 e2 : Expr)
  | constructModule (e : Expr)
  | inModule (e : Expr) (env : List (VarName × Ref))
  deriving Repr

Store and Environment

Using Mathlib's Std.HashMap or a simple association list for now:

import Mathlib.Data.Finmap

/-- Store maps references to values (or undefined) -/
abbrev Store := Std.HashMap Ref (Option ObjVal)

/-- Environment maps variable names to references -/
abbrev Env := Std.HashMap VarName Ref

/-- Program state -/
structure State where
  env : Env
  store : Store
  nextRef : Ref  -- Next available reference
  deriving Repr

/-- Program configuration (expression + state) -/
structure Config where
  expr : Expr
  state : State

Store Operations

/-- Allocate a new value in the store -/
def extendStore (σ : Store) (v : ObjVal) (next : Ref) : Store × Ref :=
  (σ.insert next (some v), next)

/-- Update an existing store location -/
def overrideStore (σ : Store) (r : Ref) (v : ObjVal) : Store :=
  σ.insert r (some v)

/-- Lookup a value in the store -/
def storeLookup (σ : Store) (r : Ref) : Option ObjVal :=
  σ.find? r |>.bind id

/-- Extend environment with new binding -/
def extendEnv (ε : Env) (x : VarName) (r : Ref) : Env :=
  ε.insert x r

/-- Lookup variable in environment -/
def envLookup (ε : Env) (x : VarName) : Option Ref :=
  ε.find? x

Substitution

/-- Substitute a reference for a local variable -/
partial def substOne (x : VarName) (r : Ref) : Expr → Expr
  | .id y .local => if x == y then .ref r else .id y .local
  | .id y .global => .id y .global  -- Never substitute globals
  | .letIn y t bound body =>
      .letIn y t (substOne x r bound)
        (if x == y then body else substOne x r body)  -- Shadowing
  | .fun_ params vararg body =>
      if x ∈ params ∨ vararg == some x
      then .fun_ params vararg body  -- Don't substitute bound vars
      else .fun_ params vararg (substOne x r body)
  | .seq e1 e2 => .seq (substOne x r e1) (substOne x r e2)
  | .ifThenElse c t e => .ifThenElse (substOne x r c) (substOne x r t) (substOne x r e)
  -- ... (recursive on all constructors)
  | e => e  -- Base cases

/-- Substitute multiple variables -/
def subst (xs : List VarName) (rs : List Ref) (e : Expr) : Expr :=
  List.foldl (fun acc (x, r) => substOne x r acc) e (xs.zip rs)

Evaluation Contexts

Following the Redex semantics exactly, we define explicit evaluation contexts. The Redex code defines 4 context types with different "stopping points":

Context	Purpose	Excludes
E	General evaluation	(none)
T	Try/exception context	nested `tryexcept`, `tryfinally`
H	Loop body (break/continue)	nested `loop`, `frame`, `tryfinally`
R	Return context	nested `frame`, `tryfinally`

For the core subset, we start with E (general context) and add the others when we implement exceptions and loops.

Evaluation Context Type

/-- Evaluation contexts (E in the Redex grammar)
    Each constructor represents a "hole" position in an expression.
    The hole is where evaluation is currently focused. -/
inductive EvalCtx where
  | hole                                           -- □
  -- Memory
  | fetch (E : EvalCtx)                            -- (fetch □)
  | setL (E : EvalCtx) (e : Expr)                  -- (set! □ e)
  | setR (v : Val) (E : EvalCtx)                   -- (set! v □)
  | alloc (E : EvalCtx)                            -- (alloc □)
  -- Sequencing & Control
  | seq (E : EvalCtx) (e : Expr)                   -- (seq □ e)
  | ifCtx (E : EvalCtx) (e₁ e₂ : Expr)             -- (if □ e₁ e₂)
  | letCtx (x : VarName) (t : ScopeType)           -- (let (x t = □) in e)
           (E : EvalCtx) (body : Expr)
  -- Functions
  | appFn (E : EvalCtx) (args : List Expr)         -- (app □ (e ...))
  | appArg (v : Val) (vs : List Val)               -- (app v (v ... □ e ...))
           (E : EvalCtx) (es : List Expr)
  | appVararg (v : Val) (vs : List Val)            -- (app v (v ...) □)
              (E : EvalCtx)
  | frame (E : EvalCtx)                            -- (frame □)
  | return_ (E : EvalCtx)                          -- (return □)
  -- Objects
  | object (E : EvalCtx) (meta : MetaVal)          -- (object □ mval)
  | getAttrL (E : EvalCtx) (attr : Expr)           -- (get-attr □ e)
  | getAttrR (v : Val) (E : EvalCtx)               -- (get-attr v □)
  | setAttrObj (E : EvalCtx) (attr val : Expr)     -- (set-attr □ e := e)
  | setAttrAttr (v : Val) (E : EvalCtx)            -- (set-attr v □ := e)
                (val : Expr)
  | setAttrVal (v₁ v₂ : Val) (E : EvalCtx)         -- (set-attr v v := □)
  -- Collections
  | listCls (E : EvalCtx) (elems : List Expr)      -- (list □ (e ...))
  | listElem (cls : Val) (vs : List Val)           -- (list v (v ... □ e ...))
             (E : EvalCtx) (es : List Expr)
  | tupleCls (E : EvalCtx) (elems : List Expr)     -- (tuple □ (e ...))
  | tupleElem (cls : Val) (vs : List Val)          -- (tuple v (v ... □ e ...))
              (E : EvalCtx) (es : List Expr)
  | setCls (E : EvalCtx) (elems : List Expr)       -- (set □ (e ...))
  | setElem (cls : Val) (vs : List Val)            -- (set v (v ... □ e ...))
            (E : EvalCtx) (es : List Expr)
  -- Primitives
  | builtinPrim (op : String) (vs : List Val)      -- (builtin-prim op (v ... □ e ...))
                (E : EvalCtx) (es : List Expr)
  -- Exceptions (for later)
  | raise (E : EvalCtx)                            -- (raise □)
  | tryExcept (E : EvalCtx) (x : VarName)          -- (tryexcept □ x e e)
              (catch_ else_ : Expr)
  | tryFinally (E : EvalCtx) (finally_ : Expr)     -- (tryfinally □ e)
  -- Loops (for later)
  | loop (E : EvalCtx) (next : Expr)               -- (loop □ e)
  -- Assignment
  | assignR (r : Ref) (E : EvalCtx)                -- (assign ref := □)
  | assignGlobal (x : VarName) (E : EvalCtx)       -- (assign (id x global) := □)
  -- Modules (for later)
  | module (E : EvalCtx) (e : Expr)                -- (module □ e)
  | constructModule (E : EvalCtx)                  -- (construct-module □)
  | inModule (E : EvalCtx) (env : Env)             -- (in-module □ ε)
  deriving Repr

Plug Function

/-- Plug an expression into an evaluation context's hole -/
def plug : EvalCtx → Expr → Expr
  | .hole, e => e
  | .fetch E, e => .fetch (plug E e)
  | .setL E e', e => .set! (plug E e) e'
  | .setR v E, e => .set! (.val v) (plug E e)
  | .alloc E, e => .alloc (plug E e)
  | .seq E e', e => .seq (plug E e) e'
  | .ifCtx E e₁ e₂, e => .ifThenElse (plug E e) e₁ e₂
  | .letCtx x t E body, e => .letIn x t (plug E e) body
  | .appFn E args, e => .app (plug E e) args
  | .appArg v vs E es, e => .app (.val v) (vs.map .val ++ [plug E e] ++ es)
  | .frame E, e => .frame (plug E e)
  | .return_ E, e => .return_ (plug E e)
  -- ... (continue for all constructors)

Specialized Contexts (T, H, R)

For exceptions, loops, and returns, we need specialized contexts that exclude certain forms:

/-- Try context T - excludes nested tryexcept/tryfinally -/
inductive TryCtx where
  | hole
  | fetch (T : TryCtx)
  | seq (T : TryCtx) (e : Expr)
  -- ... same as EvalCtx BUT excludes:
  -- | tryExcept    -- Don't catch nested try-except's raises
  -- | tryFinally   -- Don't go into try-finally

/-- Loop context H - for finding break/continue -/
inductive LoopCtx where
  | hole
  | fetch (H : LoopCtx)
  | seq (H : LoopCtx) (e : Expr)
  | tryExcept (H : LoopCtx) (x : VarName) (catch_ else_ : Expr)  -- DO include
  -- ... BUT excludes:
  -- | loop         -- Don't go into nested loops
  -- | frame        -- Don't go into nested functions
  -- | tryFinally   -- Don't go into try-finally

/-- Return context R - for finding return statements -/
inductive ReturnCtx where
  | hole
  | fetch (R : ReturnCtx)
  | seq (R : ReturnCtx) (e : Expr)
  | loop (R : ReturnCtx) (next : Expr)        -- DO include
  | tryExcept (R : ReturnCtx) (x : VarName) (catch_ else_ : Expr)  -- DO include
  -- ... BUT excludes:
  -- | frame        -- Don't go into nested functions
  -- | tryFinally   -- Don't go into try-finally

Small-Step Reduction Relation

The reduction relation uses contexts explicitly. Base rules (redexes) operate on fully-evaluated sub-expressions, and a context rule lifts them to arbitrary positions.

/-- Base reduction rules (redexes) - operate when sub-expressions are values -/
inductive StepBase : Config → Config → Prop where

  -----------------------------------------------------------------
  -- Memory Operations
  -----------------------------------------------------------------

  /-- E-Fetch: Dereference a pointer -/
  | fetch {r v σ ε n} :
      storeLookup σ r = some v →
      StepBase ⟨.fetch (.ref r), ⟨ε, σ, n⟩⟩
               ⟨.objVal v, ⟨ε, σ, n⟩⟩

  /-- E-Alloc: Allocate new heap cell -/
  | alloc {v σ ε n} :
      StepBase ⟨.alloc (.objVal v), ⟨ε, σ, n⟩⟩
               ⟨.ref n, ⟨ε, σ.insert n (some v), n + 1⟩⟩

  /-- E-Set!: Update heap cell -/
  | set! {r v σ ε n} :
      StepBase ⟨.set! (.ref r) (.objVal v), ⟨ε, σ, n⟩⟩
               ⟨.objVal v, ⟨ε, overrideStore σ r v, n⟩⟩

  -----------------------------------------------------------------
  -- Variables
  -----------------------------------------------------------------

  /-- E-GetGlobal: Lookup global variable in environment -/
  | getGlobal {x r v σ ε n} :
      envLookup ε x = some r →
      storeLookup σ r = some v →
      StepBase ⟨.id x .global, ⟨ε, σ, n⟩⟩
               ⟨.objVal v, ⟨ε, σ, n⟩⟩

  /-- E-LetGlobal: Bind global variable, extend environment -/
  | letGlobal {x v body σ ε n} :
      StepBase ⟨.letIn x .global (.objVal v) body, ⟨ε, σ, n⟩⟩
               ⟨body, ⟨extendEnv ε x n, σ.insert n (some v), n + 1⟩⟩

  /-- E-LetLocal: Bind local variable via substitution -/
  | letLocal {x v body σ ε n} :
      StepBase ⟨.letIn x .local (.objVal v) body, ⟨ε, σ, n⟩⟩
               ⟨substOne x n body, ⟨ε, σ.insert n (some v), n + 1⟩⟩

  -----------------------------------------------------------------
  -- Control Flow
  -----------------------------------------------------------------

  /-- E-Seq: Discard first value, continue with second -/
  | seq {v e₂ s} :
      StepBase ⟨.seq (.objVal v) e₂, s⟩ ⟨e₂, s⟩

  /-- E-IfTrue: Truthy condition takes then branch -/
  | ifTrue {v e₁ e₂ s} :
      truthy v = true →
      StepBase ⟨.ifThenElse (.objVal v) e₁ e₂, s⟩ ⟨e₁, s⟩

  /-- E-IfFalse: Falsy condition takes else branch -/
  | ifFalse {v e₁ e₂ s} :
      truthy v = false →
      StepBase ⟨.ifThenElse (.objVal v) e₁ e₂, s⟩ ⟨e₂, s⟩

  -----------------------------------------------------------------
  -- Functions
  -----------------------------------------------------------------

  /-- E-Fun: Create closure, allocate in store -/
  | fun_ {params vararg body σ ε n} :
      let closure := ObjVal.mk (.sym "%function")
                               (.closure params vararg body) []
      StepBase ⟨.fun_ params vararg body, ⟨ε, σ, n⟩⟩
               ⟨.ref n, ⟨ε, σ.insert n (some closure), n + 1⟩⟩

  /-- E-App: Apply function to arguments -/
  | app {r params body args σ ε n} :
      storeLookup σ r = some ⟨_, .closure params none body, _⟩ →
      params.length = args.length →
      let (σ', refs) := allocArgs σ n args
      StepBase ⟨.app (.ref r) (args.map Expr.objVal), ⟨ε, σ, n⟩⟩
               ⟨.frame (subst params refs body), ⟨ε, σ', n + args.length⟩⟩

  /-- E-Return: Return pops the frame -/
  | return_ {v s} :
      StepBase ⟨.frame (.return_ (.objVal v)), s⟩ ⟨.objVal v, s⟩

  /-- E-FramePop: Normal completion pops the frame -/
  | framePop {v s} :
      StepBase ⟨.frame (.objVal v), s⟩ ⟨.objVal v, s⟩

  -----------------------------------------------------------------
  -- Collections (allocate and return pointer)
  -----------------------------------------------------------------

  /-- E-List: Allocate list with evaluated elements -/
  | list {clsVal vs σ ε n} :
      let listObj := ObjVal.mk clsVal (.list vs) []
      StepBase ⟨.list (.objVal ⟨clsVal, .., []⟩) (vs.map (Expr.objVal ·)), ⟨ε, σ, n⟩⟩
               ⟨.ref n, ⟨ε, σ.insert n (some listObj), n + 1⟩⟩

  -- Similar for tuple, set...

/-- Full reduction: base step in any evaluation context -/
inductive Step : Config → Config → Prop where
  /-- Lift base step through evaluation context -/
  | ctx {E : EvalCtx} {e e' : Expr} {s s' : State} :
      StepBase ⟨e, s⟩ ⟨e', s'⟩ →
      Step ⟨plug E e, s⟩ ⟨plug E e', s'⟩

Exception Handling (uses T context)

  /-- E-Raise: Uncaught raise becomes error -/
  | raiseUncaught {v s} :
      StepBase ⟨.raise (.objVal v), s⟩ ⟨.err v.toVal, s⟩

  /-- E-TryCatch: Catch a raised exception using T context -/
  | tryCatch {T : TryCtx} {v x catch_ else_ s} :
      Step ⟨.tryExcept (plugT T (.raise (.objVal v))) x catch_ else_, s⟩
           ⟨.letIn x .local (.objVal v) catch_, s⟩

  /-- E-TryElse: No exception, run else branch -/
  | tryElse {v x catch_ else_ s} :
      Step ⟨.tryExcept (.objVal v) x catch_ else_, s⟩
           ⟨else_, s⟩

Loop Handling (uses H context)

  /-- E-While: Unfold while to if + loop -/
  | while {cond body else_ s} :
      Step ⟨.while cond body else_, s⟩
           ⟨.ifThenElse cond (.loop body (.while cond body else_)) else_, s⟩

  /-- E-LoopNext: Body completed, continue to next iteration -/
  | loopNext {v next s} :
      Step ⟨.loop (.objVal v) next, s⟩ ⟨next, s⟩

  /-- E-LoopBreak: Break found in H context -/
  | loopBreak {H : LoopCtx} {next s} :
      Step ⟨.loop (plugH H .break) next, s⟩ ⟨.objVal noneVal, s⟩

  /-- E-LoopContinue: Continue found in H context -/
  | loopContinue {H : LoopCtx} {next s} :
      Step ⟨.loop (plugH H .continue) next, s⟩ ⟨next, s⟩

Truthiness (Python semantics)

/-- Python truthiness rules -/
def truthy : ObjVal → Bool
  | ⟨_, .none, _⟩ => false
  | ⟨_, .num 0, _⟩ => false
  | ⟨_, .str "", _⟩ => false
  | ⟨_, .list [], _⟩ => false
  | ⟨_, .tuple [], _⟩ => false
  | ⟨_, .set [], _⟩ => false
  | _ => true

Implementation Milestones

M1: Syntax Foundation (Week 1)

Define ScopeType, VarName, Ref
Define MetaVal inductive
Define Val and ObjVal
Define Expr inductive (core subset only)
Basic Repr and DecidableEq instances

M2: Store and Environment (Week 1)

Define Store type using Std.HashMap
Define Env type
Implement extendStore, overrideStore, storeLookup
Implement extendEnv, envLookup
Define State and Config

M3: Substitution (Week 2)

Implement substOne for single variable
Implement subst for multiple variables
Handle shadowing correctly
Test with example expressions

M4: Core Reduction Rules (Week 2)

Values (already values, no step)
seq reduction
ifThenElse reduction with truthy
Congruence rules for sub-expression evaluation

M5: Memory Operations (Week 3)

M6: Functions (Week 3)

Function creation (fun_)
Function application (app)
frame and return_ handling
Argument allocation helper

M7: Multi-step Evaluation (Week 4)

Define Step* as reflexive-transitive closure
Define eval function with fuel
Example programs that evaluate to values

M8: Extensions (Future)

Key Design Decisions

1. Explicit Evaluation Contexts

Chosen: Explicit Evaluation Contexts (faithful to Redex)

The Redex semantics uses (in-hole E e) patterns extensively. We mirror this directly in Lean:

EvalCtx inductive type: Each constructor represents a context with a hole
plug : EvalCtx → Expr → Expr: Fills the hole with an expression
Step relation: Uses a single context rule that lifts StepBase through any EvalCtx

This requires:

Proving plug is injective (for determinism)
Handling the 4 context variants (E, T, H, R) for control flow
More boilerplate but direct correspondence to source semantics

The specialized contexts (T, H, R) are crucial for correct exception/loop/return handling:

T (TryCtx): Excludes nested try blocks so raise finds the right handler
H (LoopCtx): Excludes nested loops/frames so break/continue find the right loop
R (ReturnCtx): Excludes nested frames so return finds the right function

2. Store Representation

Chosen: Std.HashMap Ref (Option ObjVal)

Options considered:

List (Ref × ObjVal) - Simple but O(n) lookup
Std.HashMap - O(1) average lookup, good for execution
Mathlib.Data.Finmap - Finite maps with better proof support

We use Std.HashMap for efficiency. Can switch to Finmap if we need stronger proof automation.

3. Handling Undefined Values

The Redex semantics has undefined-val for uninitialized variables. We represent this with:

Option ObjVal in the store (None = undefined)
Or an explicit Expr.undefined constructor

4. Mutual Recursion

Expr and MetaVal are mutually recursive (closures contain expressions). In Lean 4, we can use mutual blocks or nested inductives.

Testing Strategy

Unit tests: Small expression evaluations
Property tests: Determinism, progress (well-typed don't get stuck)
Conformance tests: Port tests from lambda-py/redex/*-tests.rkt

Example test:

-- (let x = 42 in x) should evaluate to 42
example : Step*
  ⟨.letIn "x" .local (.objVal ⟨.sym "%int", .num 42, []⟩) (.id "x" .local), initState⟩
  ⟨.objVal ⟨.sym "%int", .num 42, []⟩, _⟩ := by
  sorry

Files to Create

PythonOfLean/Syntax/Expr.lean - Expression types
PythonOfLean/Syntax/Value.lean - Value types
PythonOfLean/Semantics/Store.lean - Store operations
PythonOfLean/Semantics/Env.lean - Environment operations
PythonOfLean/Semantics/State.lean - Program state
PythonOfLean/Semantics/Subst.lean - Substitution
PythonOfLean/Semantics/Step.lean - Reduction relation
PythonOfLean/Semantics/Eval.lean - Multi-step evaluation
PythonOfLean/Examples/Basic.lean - Test programs

FilesExpand file tree

PLAN.md

Latest commit

History