Hello Josh Burdick,
* Am 29.03.07 schrieb Josh Burdick:
> 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
The epigram programming language not only eschews general recursion to
keep the logic of the type system sound. It was a /design decision/ by
McBride/McKinna
http://foundations.cs.ru.nl/chitchat/slides/chit-swierstra.pdf
to default to structural recursion since the novel kind of interaction
the epigram system provides during program development relies on the
decidability of the type checking relation. Which get's lost if you
allow possibly non-terminating computations in types, as for example
Lennart Augustsson's cayenne language did.
Conor McBride usually suggests to have fix as an axiom sans
computational behaviour during type checking to answer demands for
general recursion.
http://www.haskell.org/pipermail/haskell/2004-August/014405.html
> 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.
So it could be nice to have programs which use general recursion
tagged in the type system. This has also been suggested for
epigram, taking partiality as a monadic effect building on work by
Altenkirch/Capretta/Uustalu.
http://www.cs.nott.ac.uk/~txa/talks/bctcs06.pdf
> 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
Ackerman's function has been discussed extensively on this list.
Thorsten Altenkirch showed how to define it with primitive recursion at
higher types.
http://article.gmane.org/gmane.comp.lang.epigram/100
And Conor McBride explained in detail how epigram represents a
computation of Ackerman's function internally.
http://article.gmane.org/gmane.comp.lang.epigram/104
> 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.
I'm not familiar enough with church encodings and feasible arithmetics
but you seem to want to establish something like the limit of any n-fold
function application and this is domain theory's definition of
fixpoint.
> 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.
To see how to write the factorial with the partial monad have a look at:
http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=3
Best regards,
Sebastian
