OK here's a subproblem: Fix the logic as the calculus of inductive constructions. Is the problem of determining whether a function is extensionally equal to the identity function at a given (but arbitrary) type undecidable?
So fix arbitrary X, and an arbitrary function:
f : X -> X
You want to write a program that determines whether:
forall (x : X), f x = x
Is that undecidable?
f : X -> X
You want to write a program that determines whether:
forall (x : X), f x = x
Is that undecidable?
Note that in this logic, f must always terminate! But there may be infinitely many possible x : X
• • •
Missing some Tweet in this thread? You can try to
force a refresh
