10
$\begingroup$

Constructive type theory with its basic interpretation under the curry howard correspondence consists only of total, computable functions. In the literature, some has been said on using "computational type theory" in order to represent non-termination in functional programs, yet in the papers I have come across, this does not seem to be the major motivation for the theory (For example Benton mentions non-determinism, continuations, and exceptions, without going into much detail on non-termination), so I have yet to find a paper giving a robust interpretation of non-termination using computational type theory.

Specifically, what I am looking for is a way that given a type representing a possibly non terminating computation of type $A$, $T(A)$, there should be some notion of proofs that $x : T(A)$ terminates of type $H(x)$, such that given $x:T(A)$ and $p:H(x)$, we can construct a term $\tilde x : A$.

My motivation for this is, I'd like to eventually be able to more formally relate notions in computational complexity theory to constructive type theory. Specifically, I am interested in what power as a formal theory constructive types gain with access to a halting oracle, and in order to do so, I of course need to actually have a formal notion of possible non-termination, and proofs of halting to go along with it inside a type-theoretic framework.

$\endgroup$
  • 3
    $\begingroup$ Did you look at Constable-Mendler, Recursive Definitions in Type Theory? They give a way of defining for every fixed-point recursive definition of a partial function $f$ from $A$ to $B$ a domain predicate $\mathrm{dom}(f)$ such that for $x\in A$, $\mathrm{dom}(f)(x)$ represents the type of proofs that $f$ halts at $x$. I believe this is implemented in Nuprl. $\endgroup$ – Ulrik Buchholtz Apr 12 '16 at 2:19
  • 3
    $\begingroup$ Are you looking for the delay monad? $\endgroup$ – Andrej Bauer Apr 12 '16 at 6:34
  • $\begingroup$ @UlrikBuchholtz I think that's pretty close to what I'm looking for, though I'm having some difficulty parsing through the Nuprl notation that is used in the paper -- which I am not similar with. If I understand correctly, they essentially define a partial recursive function from $A$ to $B$ (or at least, identify them with) as a total recursive function from $\{x:A | dom(f)(g) \} to B. (See the remark at the bottom of page 27) $\endgroup$ – Nathan BeDell Apr 12 '16 at 16:15
11
$\begingroup$

Because one of the principal applications of Type Theory in formalizations has been to study programing languages and computation in general, a lot of thought has gone into ways of representing possibly non-terminating programs.

I won't make a complete survey here, but I'll try and give pointers to the main thrusts of different directions.

  • The "relational" approach: you can define your hypothetical programs as relations say, $F\ x\ y$ which holds iff $f$ is defined at $x$ and $f(x)=y$. This is usually what is done with the Kleene T-predicate. This works just as well in type theory formalizations as it does in classical logic, (though of course you can't prove $\forall x (\exists y, F\ x\ y)\vee (\neg\exists y, F\ x\ y)$).

    A more sophisticated way to do this is the "Bove-Capretta" method (see Modelling Recursion in Type Theory, which for each recursive function, defines an "accessible predicate" which encodes the fact that a given computation is finite. The function definition takes an extra argument which is a proof that the given inputs are accessible. To define the function without this extra predicate, you need to prove that every possible combination of inputs is accessible.

  • The "coinductive" approach: this is possibly the most explored approach, and what Andrej's comments refer to. A computation of type $A$ is defined as the inductive type (from Andrej's link, by Capretta, Altenkirch & Uustalu:

    codata Delay A =
    | Now : A -> Delay A
    | Later (Delay A)
    

    This codes a possibly infinite stream of Later tokens ("ticks" of computation) maybe ending with a result Now a. Non-termination is equivalent to being bisimilar with the program

    loop = Later loop and termination can be defined by an inductive predicate over Delay A:

    data Terminates : Data A -> Prop =
    | Term_now : forall x, Terminates (Now x)
    | Term_later : forall d, Terminates d -> Terminates (Later d)
    

    I think the agda-istas have a lot to say about this which they call the partiality monad (see e.g. Danielsson).

  • The "partial type theory" approach: this is a bit more experimental (the theory is still being worked out), but there are some type theories that are being developed to cope with the fact that there are essentially two types of functions we want to write in type theory: the proof terms and the programs. It turns out to be tough to get a reasonable theory of these things (and retain consistency of the theory), but a serious attempt is made here by Casinghino et al, and a similar effort by Kimmel et al.

I'm sure there are other approaches I'm not aware of, and I'd be happy if someone wants to complete this list.

I should probably note that adding a termination oracle to a (consistent) type theory is a lot like adding a truth oracle for $\Pi^0_1$ sentences, with relatively well understood consequences.

There are other, quite fruitful interactions between type theory and complexity theory, usually under the umbrella of implicit computational complexity.

$\endgroup$
  • $\begingroup$ Interesting, thanks for the information! I believe the partial type theory approach is probably closest in spirit to what I am looking for -- and at the very least, the Kimmel paper seems to provide on some level specifically what I am looking for (see the typing rules for "tcast"). $\endgroup$ – Nathan BeDell Apr 12 '16 at 22:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.