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} |
Author
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...
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
@NathanielB123 @lawcho I feel like there seems to be something going on with eliminating nestedness by eliminating to higher types (the hierarchy here as in System T, i.e. every arrow left or right increases the level of the type), since this is also how one does it for Ackermann