Undecidability of equivalence

[sassa_nf]

https://en.wikipedia.org/wiki/Lambda_calculus#Undecidability_of_equivalence - it's been there all along...

There is no algorithm that takes as input two lambda expressions and outputs TRUE or FALSE depending on whether or not the two expressions are equivalent. This was historically the first problem for which undecidability could be proven.
...Building on earlier work by Kleene and constructing a Gödel numbering for lambda expressions, [Church] constructs a lambda expression e that closely follows the proof of Gödel's first incompleteness theorem. If e is applied to its own Gödel number, a contradiction results.
(Now the entire discussion about equality in lambda calculus looks pretty funny)

Comments

[juan_gandhi]

Sure. I never meant equivalence or extensional equality. Just any equivalence, e.g. intentional equality. Like

def sameFunction[A,B](f: A=>B, g: A=>B): Boolean = f eq g

This does not seem to be doable in lambda either.

Anyway, It seems like this one is a good reading: https://intuitionistic.files.wordpress.com/2010/07/nordstrom-et-al-programming.pdf

[sassa_nf]

That book seems vaguely familiar. (Probably my first read with formal proofs with sequents. I remember grappling with the idea of introductions and eliminations.)

Fortunately, Martin Lof knew equality would be a problem, so "To know A is a set is to know how to form the canonical elements in the set and under what conditions two canonical elements are equal". So all terms come with a type and intensional equality defined.

Understanding Agda after that is fairly straightforward.