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

Credit to: https://news.ycombinator.com/item?id=15186988