# Any example of a pathological normalization case?

(Stephen Weber) #1

People always say there are simple-ish lambda calculus expressions which take an absurdly long time to normalize – effectively meaning that even if we know they terminate they run past all worthwhile resources. I wonder if anyone has an example of such an expression for Dhall.

(Ari Becker) #2

Not a great example:

`time dhall <<< 'https://raw.githubusercontent.com/coralogix/dhall-concourse/v0.3.0/default/package.dhall sha256:8908ad8da681c45af47accf601124608b68c7b08a18795bca579f94161acf3a4'`

Currently takes 35 seconds. Adding `&>/dev/null` is still about 22 seconds. The better examples are pipelines which actually use those defaults, which take 40+ minutes, but unfortunately I can’t make those public yet. If you watch the scroll, you see that the normal forms are pretty large.

Hope it’s better than nothing if no-one else chimes in.

(Gabriel Gonzalez) #3

Here’s the Ackermann function encoded in pure lambda calculus, which will basically never complete:

``````let Peano
: Type
= ∀(Peano : Type) → ∀(Succ : Peano → Peano) → ∀(Zero : Peano) → Peano

let one
: Peano
= λ(Peano : Type) → λ(Succ : Peano → Peano) → λ(Zero : Peano) → Succ Zero

let iterate
: (Peano → Peano) → Peano → Peano
=   λ(f : Peano → Peano)
→ λ(n : Peano)
→ λ(Peano : Type)
→ λ(Succ : Peano → Peano)
→ λ(Zero : Peano)
→ n Peano@1 f (f one) Peano Succ Zero

let increment
: Peano → Peano
=   λ(n : Peano)
→ λ(Peano : Type)
→ λ(Succ : Peano → Peano)
→ λ(Zero : Peano)
→ n Peano Succ (Succ Zero)

let ackermann = λ(m : Peano) → m (Peano → Peano) iterate increment

let ten
: Peano
=   λ(Peano : Type)
→ λ(Succ : Peano → Peano)
→ λ(Zero : Peano)
→ Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))

in  ackermann ten ten
``````