I have a question about an idea for adding "almost" a fixpoint to an otherwise strongly-normalizing language. I'm going to write CC here to mean the Calculus of Constructions (without inductive types), but I think the idea is relevant to Epigram, since it's strongly normalizing.
CC relies on strong normalization for its soundness, so you can't just toss an axiom like fix : forall T. (T -> T) -> T into the context, because then all types are inhabited, something like "27 < 4" is trivially provable, and (for instance) any proofs you use for array bounds are useless. However, in CC, Ackerman's function is definable. I omit the definition here (because I don't know it :/), so you should be able to write reallyHugeNumber = ackerman 20 20 : forall T. (T -> T) -> (T -> T) It seems like, at this point, a proof that uses "reallyHugeNumber" is going to be sound. But in practical terms, the "zero" arg will never get called; "reallyHugeNumber" will just call the "successor" arg a very large number of times. In that case, would it be sound to introduce a constant inf : forall T. (T -> T) -> (T -> T) which just always calls its "successor" arg infinitely many times? It seems like doing so would allow potentially unbounded recursion without compromising proof soundness, for types which are inhabited. It's sort of funny-looking, though: to write a factorial function, for instance, you have to give "inf" an int, which doesn't get used for anything. Still, since Epigram is right between programming languages and proof checkers, it seemed worth asking: does this make sense? (The idea is a lot like Herman Geuvers, Erik Poll and Jan Zwanenburg. Safe Proof Checking in Type Theory with Y, Proceedings of CSL'99, the 13 International Workshop on Computer Science Logic, Madrid, Spain. Pages 439--452. except there, the Y has to be reduced away before the proof is accepted. It also seems a bit like the idea of "admissable types" in NuPRL.) Josh Burdick
