Created
January 12, 2026 12:40
-
-
Save cxandru/91b1497ca735bb251b688add18512c39 to your computer and use it in GitHub Desktop.
Alexandru's recursion razor
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| The question is how to encode the mutual nested recursion happening in "razor" using structured recursion (ideally recursive coalgebras) | |
| \begin{code} | |
| open import Level using (Level;_⊔_;0ℓ) | |
| open import Relation.Nullary | |
| open import Relation.Binary.PropositionalEquality.Core | |
| module Razor where | |
| open import Data.Nat | |
| open import Data.Product | |
| open import Function.Base | |
| open import Data.String | |
| mutual | |
| data Expr : Set where | |
| _:+:_ : Expr → Expr → Expr | |
| Var : String → Expr | |
| Lit : ℕ → Expr | |
| Let_In : Assgt → Expr → Expr | |
| data Assgt : Set where | |
| _↦_ : String → Expr → Assgt | |
| Env : Set | |
| Env = String → ℕ | |
| \end{code} | |
| %<*razor> | |
| \begin{code} | |
| mutual | |
| evA : Env → Assgt → Env | |
| evE : Env → Expr → ℕ | |
| evA env ( x ↦ expr ) = λ y → case x ≈? y of | |
| λ{ (yes _) → evE env expr | |
| ; (no _) → env y } | |
| evE env (x :+: y) = evE env x + evE env y | |
| evE env (Var x) = env x | |
| evE env (Lit n) = n | |
| evE env (Let assgt In expr) = evE (evA env assgt) expr | |
| \end{code} | |
| %</razor> | |
| \begin{code} | |
| -- decode the mutual recursion: | |
| data EoA : Set where | |
| E : EoA | |
| A : EoA | |
| data AST : EoA → Set where | |
| _:+:_ : AST E → AST E → AST E | |
| Var : String → AST E | |
| Lit : ℕ → AST E | |
| Let_In : AST A → AST E → AST E | |
| _↦_ : String → AST E → AST A | |
| ev : Env → {i : EoA} → AST i → (case i of λ{A → Env ; E → ℕ}) | |
| ev env (x :+: y) = ev env x + ev env y | |
| ev env (Var x) = env x | |
| ev env (Lit n) = n | |
| ev env (Let assgt In expr) = ev (ev env assgt) expr | |
| ev env (x ↦ expr) = λ y → case x ≈? y of | |
| λ{ (yes _) → ev env expr | |
| ; (no _) → env y } | |
| \end{code} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Ooh that's an interesting point. So I guess the concrete question is: can you write this interpreter with only primitive recursion? I'm not sure...