<p>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.</p>
<p>I won't make a complete survey here, but I'll try and give pointers to the main thrusts of different directions.</p>
<ul>
<li><strong>The &quot;relational&quot; approach:</strong> you can define your hypothetical programs as relations say, <span class="math-container">$F\ x\ y$</span> which holds iff <span class="math-container">$f$</span> is defined at <span class="math-container">$x$</span> and <span class="math-container">$f(x)=y$</span>. This is usually what is done with the <a href="https://en.wikipedia.org/wiki/Kleene%27s_T_predicate" rel="nofollow noreferrer">Kleene T-predicate</a>. This works just as well in type theory formalizations as it does in classical logic, (though of course you can't prove <span class="math-container">$\forall x (\exists y, F\ x\ y)\vee (\neg\exists y, F\ x\ y)$</span>).</li>
</ul>
<p>A more sophisticated way to do this is the &quot;Bove-Capretta&quot; method (see <a href="http://www.duplavis.com/venanzio/publications/General_Recursion_MSCS_2005.pdf" rel="nofollow noreferrer"><em>Modelling Recursion in Type Theory</em></a>, which for each recursive function, defines an &quot;accessible predicate&quot; 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.</p>
<ul>
<li><p><strong>The &quot;coinductive&quot; approach:</strong> this is possibly the most explored approach, and what Andrej's comments refer to. A computation of type <span class="math-container">$A$</span> is defined as the inductive type (from Andrej's <a href="https://www.cs.ox.ac.uk/ralf.hinze/WG2.8/22/slides/tarmo.pdf" rel="nofollow noreferrer">link</a>, by Capretta, Altenkirch &amp; Uustalu:</p>
<pre><code>  codata Delay A =
  | Now : A -&gt; Delay A
  | Later (Delay A)
</code></pre>
</li>
</ul>
<p>This codes a possibly infinite stream of <code>Later</code> tokens (&quot;ticks&quot; of computation) maybe ending with a result <code>Now a</code>. Non-termination is equivalent to being bisimilar with the program</p>
<pre><code>loop = Later loop
</code></pre>
<p>and termination can be defined by an inductive predicate over <code>Delay A</code>:</p>
<pre><code>    data Terminates : Delay A -&gt; Prop =
    | Term_now : forall x, Terminates (Now x)
    | Term_later : forall d, Terminates d -&gt; Terminates (Later d)
</code></pre>
<p>I think the agda-istas have a lot to say about this which they call the <strong>partiality monad</strong> (see e.g. <a href="http://www.cse.chalmers.se/%7Enad/publications/danielsson-semantics-partiality-monad.html" rel="nofollow noreferrer">Danielsson</a>).<span class="math-container">$ $</span></p>
<ul>
<li><strong>The &quot;partial type theory&quot; approach</strong>: 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 <a href="http://www.tyconmismatch.com/papers/combining-TR.pdf" rel="nofollow noreferrer">Casinghino <em>et al</em></a>, and a similar effort by <a href="http://homepage.cs.uiowa.edu/%7Eastump/papers/pi13.pdf" rel="nofollow noreferrer">Kimmel <em>et al</em></a>.</li>
</ul>
<p>I'm sure there are other approaches I'm not aware of, and I'd be happy if someone wants to complete this list.</p>
<p>I should probably note that adding a termination oracle to a (consistent) type theory is a lot like adding a truth oracle for <span class="math-container">$\Pi^0_1$</span> sentences, with relatively well understood consequences.</p>
<p>There are other, quite fruitful interactions between type theory and complexity theory, usually under the umbrella of <a href="http://www.cs.unibo.it/%7Emartini/BISS/martini-1.pdf" rel="nofollow noreferrer">implicit computational complexity</a>.</p>

CC BY-SA 3.0
2016-04-12T22:38:23.940Z
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").
Nathan BeDell
CC BY-SA 4.0
2016-04-12T17:45:42.730Z
2021-06-12T19:10:51.507Z
2021-06-12T19:10:51.507Z
cody
<p>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 <a href="https://research.microsoft.com/en-us/um/people/nick/jfp.ps">Benton</a> 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.</p>

<p>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 <em>proofs that $x : T(A)$ terminates</em> of type $H(x)$, such that given $x:T(A)$ and $p:H(x)$, we can construct a term $\tilde x : A$. </p>

<p>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.</p>

CC BY-SA 3.0
2016-04-12T02:19:39.157Z
Did you look at Constable-Mendler, [Recursive Definitions in Type Theory](http://www.nuprl.org/documents/Constable/RecursiveDefinitions.html)? 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.
Ulrik Buchholtz
CC BY-SA 3.0
2016-04-12T06:34:50.727Z
Are you looking for [the delay monad](https://www.cs.ox.ac.uk/ralf.hinze/WG2.8/22/slides/tarmo.pdf)?
Andrej Bauer
CC BY-SA 3.0
2016-04-12T16:15:41.417Z
@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)
Nathan BeDell
<lo.logic><type-theory><oracles><halting-problem>
Is there a good notion of non-termination and halting proofs in type theory?
Nathan BeDell
# Is there a good notion of non-termination and halting proofs in type theory?

(Asked by: username_0 on 2016-04-12)

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](https://research.microsoft.com/en-us/um/people/nick/jfp.ps) 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.

**Tags:** lo.logic, type-theory, oracles, halting-problem
> **Comments:**
> **username_1**: Did you look at Constable-Mendler, [Recursive Definitions in Type Theory](http://www.nuprl.org/documents/Constable/RecursiveDefinitions.html)? 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.  
> **username_2**: Are you looking for [the delay monad](https://www.cs.ox.ac.uk/ralf.hinze/WG2.8/22/slides/tarmo.pdf)?  
> **username_0**: @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)  

---

## 1 answers

### Answer by username_3 on 2016-04-12. Score: 13 | Accepted answer

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 : Delay 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.

> **Comments:**
> **username_0**: 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").  

---

