Last active
June 17, 2023 10:48
-
-
Save AndrasKovacs/6b1270d9edb702641f42fd6440f0f750 to your computer and use it in GitHub Desktop.
Minimal environment machine normalization with a fixpoint operator
This file contains 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
{-# language Strict, BangPatterns #-} | |
data Tm = Var Int | App Tm Tm | Lam Tm | Fix Tm deriving (Show, Eq) | |
data Val = VVar Int | VApp Val Val | VLam [Val] Tm | VFix [Val] Tm | |
isCanonical :: Val -> Bool | |
isCanonical VLam{} = True | |
isCanonical _ = False | |
eval :: [Val] -> Tm -> Val | |
eval vs (Var x) = vs !! x | |
eval vs (App t u) = case (eval vs t, eval vs u) of | |
(VLam vs t, !u) -> eval (u:vs) t | |
(VFix vs t, u) | isCanonical u -> eval (u:VFix vs t:vs) t | |
(t, u) -> VApp t u | |
eval vs (Lam t) = VLam vs t | |
eval vs (Fix t) = VFix vs t | |
quote :: Int -> Val -> Tm | |
quote l (VVar x) = Var (l - x - 1) | |
quote l (VApp t u) = App (quote l t) (quote l u) | |
quote l (VLam vs t) = Lam (quote (l + 1) (eval (VVar l:vs) t)) | |
quote l (VFix vs t) = Fix (quote (l + 2) (eval (VVar (l+1):VVar l:vs) t)) | |
nf :: Tm -> Tm | |
nf = quote 0 . eval [] | |
-- examples | |
------------------------------------------------------------ | |
instance Num Tm where | |
fromInteger = Var . fromInteger | |
(+) = undefined; (*) = undefined | |
abs = undefined; signum = undefined; (-) = undefined | |
($$) = App | |
infixl 7 $$ | |
-- Church natural numbers | |
z = Lam $ Lam $ 0 | |
s = Lam $ Lam $ Lam $ 1 $$ (2 $$ 1 $$ 0) | |
add = Lam $ Lam $ Lam $ Lam $ 3 $$ 1 $$ (2 $$ 1 $$ 0) | |
mul = Lam $ Lam $ Lam $ Lam $ 3 $$ (2 $$ 1) $$ 0 | |
n5 = s $$ (s $$ (s $$ (s $$ (s $$ z)))) | |
n10 = add $$ n5 $$ n5 | |
n100 = mul $$ n10 $$ n10 | |
-- Scott naturals | |
z' = Lam $ Lam $ 0 | |
s' = Lam $ Lam $ Lam $ 1 $$ 2 | |
-- recursive Scott addition | |
-- add' = fix rec a. case a of | |
-- S a' -> \b. S (rec a' b) | |
-- Z -> \b.b | |
add' = Fix $ 0 $$ (Lam $ Lam $ s' $$ (3 $$ 1 $$ 0)) $$ (Lam $ 0) | |
n5' = s' $$ (s' $$ (s' $$ (s' $$ (s' $$ z')))) | |
n10' = add' $$ n5' $$ n5' | |
n20' = add' $$ n10' $$ n10' | |
-- recursive Scott-to-Church conversion | |
-- s2c = fix rec a. case a of | |
-- S a' -> s (rec a') | |
-- Z -> z | |
s2c = Fix $ 0 $$ (Lam $ s $$ (2 $$ 0)) $$ z | |
test :: Bool | |
test = nf (s2c $$ n10') == nf n10 |
Ah, now I see it. So basically, we only evaluate Fix
when we know that it's applied to an argument that can determine control flow (by some computation on it), so as to not unfold inner recursive calls indefinitely. Thanks for the explanation!
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Right now it doesn't. Before I added the
isCanonical
condition, it looped because neither fixpoint combinators nor recursive definitions have normal forms with unrestricted unfolding. For a variablex
,fix f x
reduced tof (fix f x)
which reduced tof (f (fix f x))
and so on. If a recursive definition is terminating, it only makes recursive calls with smaller arguments than the input. If the argument tofix f
is neutral, no computation can make progress on it, so unfolding will not terminate. If the argument is canonical, the total recursive definitions necessarily make progress on it and only make recursive calls on smaller values, so unfolding will either terminate eventually, or hit a neutral value, in which case thefix f x
application itself is blocked.Btw, in untyped lambda calculus it is not actually true that every function is structurally larger than any of its result values, so this gist can still do infinite
fix
unfolding. In Coq however, the type system ensures (with some exotic exceptions) that a function is always larger than its results.To be more precise, we want that the ordering on values which is generated by
f
is larger thanf x
for anyx
Is well-founded.