3
$\begingroup$

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

$\endgroup$
  • 3
    $\begingroup$ What is a coprogram? $\endgroup$ – Dave Clarke Nov 2 '14 at 13:42
  • $\begingroup$ In Total Functional Programming terminology, a program terminates with useful input, while a coprogram doesn't necessarily terminates, and repeatedly produces useful input. $\endgroup$ – Carl Patenaude Poulin Dec 10 '14 at 13:28
  • $\begingroup$ Can you modify the question to reflect this definition? $\endgroup$ – Dave Clarke Dec 10 '14 at 13:37
  • $\begingroup$ Done. I'm curious though, do you really think it fits the format of this forum to explain standard terminology? $\endgroup$ – Carl Patenaude Poulin Dec 10 '14 at 14:11
  • $\begingroup$ 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. $\endgroup$ – Dave Clarke Dec 10 '14 at 15:36
5
$\begingroup$

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.

$\endgroup$
3
$\begingroup$

You could find a few examples in Danielsson's papers, such as:

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

$\endgroup$

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.