Minimal environment machine normalization with a fixpoint operator

FixNf.hs

{-# 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

Question: if I normalize \x. add' x it will be an infinite loop, correct? Since the fix is applied to something, leading to the recursive call to be applied immediately.

I just tested nf (Lam $ App (Fix $ 0 $$ (Lam $ Lam $ s' $$ (3 $$ 1 $$ 0)) $$ (Lam $ 0)) 0) and it does give a stack overflow.

You're right. I fixed the source, adding the rule that fixpoints only reduce when applied to canonical arguments. This rule is actually in Coq as well (which is a standard example for a core language with fixpoints), I omitted it by mistake.

Why does fix loop forever when applied to a non-canonical value?

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 variable x, fix f x reduced to f (fix f x) which reduced to f (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 to fix 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 the fix 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

• All constructors are larger than their fields
• f is larger than f x for any x

Is well-founded.

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!