SmithParadoxCan be loaded using File.import "smith-paradox-load.iml";
Smith’s paradox [1] is a proof that there exist non-admissible types, that is, types that cannot be used with fixpoint induction.
inadmissible_type : exists (a : U 0) . not (admiss a)
One such type is the type of definitely partial functions from nat
to unit. (By definitely partial, we mean not only that the
function might not be total, but that it is definitely not total.)
{ h : nat -> partial unit | not (forall x . halts (h x)) }
Let T be this type, and let f be the function:
fn g x . if x =? 0 then () else g (x - 1)
Since f defers to its argument g, it preserves definite
partiality. Thus one can show that f : partial T -> partial T. If
T were admissible, we could conclude by fixpoint induction that
fix f : partial T. However fix f clearly halts, so it would
follow that fix f : T. That would mean fix f is a definitely
partial function, but it is easy to show that fix f is actually
total.
[1] Scott Fraser Smith. Partial Objects in Type Theory. Ph.D. dissertation, Cornell University. 1989.