<p>To expand on pedagand's answer: <strong>productivity</strong> is the term used for the computational dual (in some precise sense) of termination. Formally, a program <code>f : CoData</code> is <em>productive</em> if running the computation <code>f</code> <em>eventually</em> produces a constructor of <code>CoData</code>, and every (recursive) sub-term of that constructor is also productive.</p>

<p>For example</p>

<pre><code>primes = filterBy prime [0..]
</code></pre>

<p>in haskell is productive, since there is an infinite number of prime numbers and so computing primes will always eventually produce a <code>cons</code> constructor.</p>

<p>There has been a number of works on using types to check for productivity of a given definition. One nice overview is Abel, <a href="http://www2.tcs.ifi.lmu.de/~abel/publications.html#tcs04">Iteration and Coiteration Schemes for Higher-Order and Nested Datatypes</a> from 2005.</p>

CC BY-SA 3.0
2014-11-03T19:54:03.347Z
2014-11-03T19:54:03.347Z
cody
<p>You could find a few examples in <a href="http://www.cse.chalmers.se/~nad/publications/" rel="nofollow">Danielsson's papers</a>, such as:</p>

<ul>
<li><a href="http://www.cse.chalmers.se/~nad/publications/danielsson-parser-combinators.pdf" rel="nofollow">Total parser combinators</a></li>
<li><a href="http://www.cse.chalmers.se/~nad/publications/danielsson-semantics-partiality-monad.pdf" rel="nofollow">Operational Semantics Using the Partiality Monad</a></li>
</ul>

<p>The key idea is to use the productivity of greatest fixpoints to guarantee liveness ("eventually something happens").</p>

CC BY-SA 3.0
2014-11-03T18:10:17.087Z
2014-11-03T18:10:17.087Z
pedagand
<p>Clarification: in Total Functional Programming terminology, a program terminates with useful input, while a coprogram doesn't necessarily terminates, and repeatedly produces useful input.</p>

<p>I am investigating the relationship between model checking and type theory. <a href="http://www.cs.ucla.edu/~palsberg/paper/esop05.pdf" rel="nofollow">It is straightforward to encode safety properties in the type of a program</a>. It seems like typing coprograms would be the best way to check liveness properties, but where is the literature on the subject? I can't find any papers about the general case.</p>

CC BY-SA 3.0
2014-11-02T13:42:59.513Z
What is a coprogram?
Dave Clarke
CC BY-SA 3.0
2014-12-10T13:28:44.227Z
In Total Functional Programming terminology, a program terminates with useful input, while a coprogram doesn't necessarily terminates, and repeatedly produces useful input.
Carl Patenaude Poulin
CC BY-SA 3.0
2014-12-10T13:37:42.407Z
Can you modify the question to reflect this definition?
Dave Clarke
CC BY-SA 3.0
2014-12-10T14:11:44.357Z
Done. I'm curious though, do you really think it fits the format of this forum to explain standard terminology?
Carl Patenaude Poulin
CC BY-SA 3.0
2014-12-10T15:36:29.663Z
It was a bit of a blunt reformulation of the question. Is it standard terminology? Google didn't reveal anything and your link didn't use the word. None of the papers linked to in the answers use the word.
Dave Clarke
CC BY-SA 3.0
2014-12-10T18:59:51.887Z
David A. Turner did a neat little bit of work in this subject at the end of his career. google/goole scholar "Elementary Strong Functional Programming". In the series of papers on this he gives an abstract interpretation of the kind of language is try to describe. This abstract interpretation allows us to say "yes this corecurisve function is productive" or "this might not be productive". I'd imagine this has pretty deep connections to model checking.
Jake
<type-theory><functional-programming><model-checking>
Typechecking liveness properties of coprograms
Carl Patenaude Poulin
# Typechecking liveness properties of coprograms

(Asked by: username_0 on 2014-11-01)

Clarification: in Total Functional Programming terminology, a program terminates with useful input, while a coprogram doesn't necessarily terminates, and repeatedly produces useful input.

I am investigating the relationship between model checking and type theory. [It is straightforward to encode safety properties in the type of a program](http://www.cs.ucla.edu/~palsberg/paper/esop05.pdf). It seems like typing coprograms would be the best way to check liveness properties, but where is the literature on the subject? I can't find any papers about the general case.

**Tags:** type-theory, functional-programming, model-checking
> **Comments:**
> **username_1**: What is a coprogram?  
> **username_0**: In Total Functional Programming terminology, a program terminates with useful input, while a coprogram doesn't necessarily terminates, and repeatedly produces useful input.  
> **username_1**: Can you modify the question to reflect this definition?  
> **username_0**: Done. I'm curious though, do you really think it fits the format of this forum to explain standard terminology?  
> **username_1**: It was a bit of a blunt reformulation of the question. Is it standard terminology? Google didn't reveal anything and your link didn't use the word. None of the papers linked to in the answers use the word.  
> **username_2**: David A. Turner did a neat little bit of work in this subject at the end of his career. google/goole scholar "Elementary Strong Functional Programming". In the series of papers on this he gives an abstract interpretation of the kind of language is try to describe. This abstract interpretation allows us to say "yes this corecurisve function is productive" or "this might not be productive". I'd imagine this has pretty deep connections to model checking.  

---

## 2 answers

### Answer by username_3 on 2014-11-03. Score: 5 | Accepted answer

To expand on pedagand's answer: productivity is the term used for the computational dual (in some precise sense) of termination. Formally, a program f : CoData is productive if running the computation f eventually produces a constructor of CoData, and every (recursive) sub-term of that constructor is also productive.
For example
primes = filterBy prime [0..]

in haskell is productive, since there is an infinite number of prime numbers and so computing primes will always eventually produce a cons constructor.
There has been a number of works on using types to check for productivity of a given definition. One nice overview is Abel, Iteration and Coiteration Schemes for Higher-Order and Nested Datatypes from 2005.


---

### Answer by username_4 on 2014-11-03. Score: 3

You could find a few examples in [Danielsson's papers](http://www.cse.chalmers.se/~nad/publications/), such as:

* [Total parser combinators](http://www.cse.chalmers.se/~nad/publications/danielsson-parser-combinators.pdf)
* [Operational Semantics Using the Partiality Monad](http://www.cse.chalmers.se/~nad/publications/danielsson-semantics-partiality-monad.pdf)

The key idea is to use the productivity of greatest fixpoints to guarantee liveness ("eventually something happens").


---

