apfelmus@quantentunnel.de writes:
Besides, having
let q = FinCons 3 q in q
not being _|_ crucially depends on memoization.
Does it? Mentally I translate that as let q = Y (\q -> FinCons 3 q) in q => Y (\q-> FinCons 3 q) => (\q -> FinCons 3 q) (Y (\q-> FinCons 3 q)) => FinCons 3 (Y (\q -> FinCons 3 q)) which, assuming a plausible lambda expression for FinCons, is a soluble term.
Even with the characterization by WHNF,
let q x = FinCons 3 (q x) in q ()
is _|_.
Again q = Y(\q x -> FinCons 3 (q x)) so q () => Y(\q x -> FinCons 3 (q x)) () => (\q x -> FinCons 3 (q x))(Y(\q x -> FinCons 3 (q x))) () => (\x -> FinCons 3 (Y(\q y-> FinCons 3 (q y)) x)) () => FinCons 3 (Y(\q x -> FinCons 3 (q x)) () ) which is in WHNF (and soluble too) -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk