The Blog of Bob Rubbens
One morning the ChatGPT
Decided to go gaslight me
I had wrote
... (c (ChurchNat × ChurchNat) succ_hist (c, c)) ...
And got stuck, passing c cyclicly.
I directed myself at ChatGPT
And asked, “In the context of church encoding, is the predecessor
function typable in dependent type theory?”
“Short answer: it depends on
impredicativity.”
It lectured me studiously
“Define ∀A:Type. (A → A) → A → A as
C”
“Then pred : C → C does not type predicatively”
“Assuming impredicavitity”
“The classic term
λn f x. n (λr i. i (r f)) (λf. x) (λu. u) is typable,
most possibly
“But mind you, evaluating it is costly
”Resolve this with additional machinery”
Distraught, I knew, woe is me
This is too much complexity
To the Lean prover zulip I flee’d
And asked for a little mercy
“Oh please, community, give me”
“The insight to this problem that is key”
Then, a wise mathematician decreed,
“Maybe
you meant to write
c (ChurchNat × ChurchNat) succ_hist (zero, zero)?”
Generated with BYOB.
License: CC-BY-SA.
This page is designed to last.
