<p>(Sorry for the blatant self-advertisement that follows!)</p>

<p>In addition to what was already said, you should really check out our recent TOPLAS paper (<a href="https://doi.org/10.1145/3285955" rel="nofollow noreferrer">https://doi.org/10.1145/3285955</a>), which deals with extensions of System F with (co)inductive types (among other things). In the first part of the paper we define a strongly-normalizing language that can deal with Scott encoding. In particular, pure <span class="math-container">$\lambda$</span>-calculus (specialized) fixpoints/recursors/iterators for Scott-encoded datatypes can be defined (and typed) in the system. We actually only give one for natural numbers (which is due to Parigot), but it seems that this should generalize easily to other datatypes. And they compute with the expected complexity as far as I remember. Note that our system also supports "Scott-encoded" codata types. For instance, we are able to type a (strongly-normalizing) coiterator for a form of streams.</p>

<p>On the technical side, quantifiers as well as (co)inductive types are handled using subtyping exclusively, which yields a syntax-directed type system that can be implemented easily. Although type-checking is most certainly undecidable here, type annotations can be used to help the system when it does not succeed in finding a proof directly (in practice, very few annotations seem to be required). To handle (sized) (co)inductive types, we rely on a cyclic (subtyping) proof mechanism. Well-foundedness is checked using a variation of the size-change principle of Lee, Jones and Ben-Amram. (In the later part of the paper, cyclic proofs are also used for typing derivations in order to type a general fixpoint.)</p>

<p>Here are the relevant links:</p>

<ul>
<li><a href="https://doi.org/10.1145/3285955" rel="nofollow noreferrer">https://doi.org/10.1145/3285955</a> (paper),</li>
<li><a href="https://github.com/rlepigre/subml/" rel="nofollow noreferrer">https://github.com/rlepigre/subml/</a> (implementation),</li>
<li><a href="https://rlepigre.github.io/subml/" rel="nofollow noreferrer">https://rlepigre.github.io/subml/</a> (online interpreter).</li>
</ul>

<p><strong>edit:</strong> I forgot to say that our system does not require any of the usual positivity or semi-continuity conditions. Our notion of subtyping is fine-grained enough to reject unwanted examples.</p>

CC BY-SA 4.0
2019-05-07T14:01:47.797Z
Thanks! Very interesting paper and provides a direct answer to my question :)
Labbekak
CC BY-SA 4.0
2019-05-07T08:34:14.830Z
2019-05-07T08:44:30.810Z
2019-05-07T08:44:30.810Z
Rodolphe Lepigre
<p>I'll first point you to <a href="http://lucacardelli.name/Papers/Notes/scott2.pdf" rel="noreferrer">Types for the Scott Numerals</a> by Plotkin, Cardelli and Abadi, where they show how to encode Scott numerals in plain old system F. This at least shows that you can write the "natural" recursion principles on Scott numerals, and because they correspond to recursors in this encoding, they are guaranteed to terminate.</p>

<p>However, if you want to work directly with the recursive type formulation, you can apply the classical theory of termination of system F augmented with the theory of positive inductive types, comprehensively treated in Ralph Matthes' <a href="https://www.irit.fr/~Ralph.Matthes/dissertation/matthesdiss.pdf" rel="noreferrer">dissertation</a>, admittedly a technical read.</p>

<p>I'm not 100% sure those techniques apply here though. I think the recursor you'd get for the Scott encoding would be something like</p>

<pre><code>recNat : forall P. ((forall t. t -&gt; (P -&gt; t) -&gt; t) -&gt; P) -&gt; (Nat -&gt; P)
</code></pre>

<p>For fixing ideas I wrote a definition in Haskell which was a bit tedious:</p>

<pre><code>rectNat f n = f $ \z s -&gt; n z (\ n' -&gt; s (recNat f n'))
</code></pre>

<p>Of course in a Matthes like system, the recursor is primitive and the Haskell definition is simply the operational semantics of the recursor.</p>

<p>and you would write addition by specializing <code>P</code> to <code>Nat -&gt; Nat</code> and implementing the first argument of <code>recNat</code> by:</p>

<pre><code>\n -&gt; n (\m -&gt; m) (\add_n m -&gt; succ $ add_n m)
</code></pre>

<p>which I think works out to the correct addition when applied to the recursor.</p>

<p>If you're really adverse to recursors, you can apply standard termination analysis techniques in system F or Calculus of constructions, see e.g. Abel's <a href="http://www2.tcs.ifi.lmu.de/~abel/diss.pdf" rel="noreferrer">dissertation</a> which is a real tour-de-force.</p>

<hr>

<p>Finally, I must caution you against a strange counter example in the realm of recursion with positive inductive types: consider the type</p>

<pre><code>I = (forall t. (t -&gt; t)) -&gt; I
</code></pre>

<p>which is positive, since a fortiori it does not even contain recursive arguments! Then one might be tempted to accept the recursive function:</p>

<pre><code>Y :: I -&gt; I
Y i = i Y i
</code></pre>

<p>There is no obvious reason to reject this program, since <code>Y</code> is not being recursively applied to any smaller arguments. However, applying <code>Y</code> to the identity function will loop.</p>

<p>All this to say that there are strange counter-examples when dealing with positive inductive types in impredicative settings. However, Scott encodings with structural recursive functions do not seem to trigger these counter-examples, and I believe that they are handled by the standard theory of termination from the literature.</p>

CC BY-SA 4.0
2019-05-04T19:27:43.080Z
Thanks a lot! I think "A Polymorphic Lambda-Calculus with Sized Higher-Order Types" might contain what I'm after. The reason I asked this question is because I implemented binary numerals and I could not figure out how to write addition efficiently (https://stackoverflow.com/questions/55772053/addition-for-binary-natural-numbers-using-primitive-recursion/55772685#55772685). It turns out (as far as I know) that I need more than primitive recursion to get an efficient implementation! So Church/Parigot encodings are not enough, I want to be more free in what kind of recursion I use.
Labbekak
CC BY-SA 4.0
2019-05-05T15:26:47.210Z
@Labbekak certainly sized types are quite flexible, but somehow I feel like fast (or at least linear time) addition of binary numbers should be possible with primitive recursion, at least depending on endianness. Might be a good question for cs.stackexchange!
cody
CC BY-SA 4.0
2019-05-05T18:33:23.170Z
Thanks, I'll ask that question on cs.stackexchange, I'm also thinking now that it might be possible. Thanks for your answer!
Labbekak
CC BY-SA 4.0
2019-05-03T19:00:25.347Z
2019-05-03T19:00:25.347Z
cody
<p>Is there any research on termination analysis on Scott-encodings in System F with positive-recursive types.
All papers I have found use languages with constructors and case analysis (for example <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.44.3494&amp;rep=rep1&amp;type=pdf" rel="noreferrer">foetus</a>).
But given that we can encode any ADT as pure lambdas, by defining an ADT as it's case analysis function, is it still possible to do termination checking similar to how it is done for ADTs?</p>

<p>For example we can encode the natural numbers as:</p>

<pre><code>type Nat = forall t. t -&gt; (Nat -&gt; t) -&gt; t
zero = \z s -&gt; z
succ n = \z s -&gt; s n
</code></pre>

<p>and then define addition like:</p>

<pre><code>add n m = n m (\n' -&gt; succ (add n' m))
</code></pre>

<p>Is it still possible to analyze the recursive calls for termination?
I am aware of Church-encodings but I am interested in structural recursion specifically.</p>

CC BY-SA 4.0
2019-05-02T13:09:32.223Z
Did you mean `Nat = forall t. t -> (t -> t) -> t` instead? Otherwise you'd need recursive types...
cody
CC BY-SA 4.0
2019-05-02T13:11:56.393Z
Ooops, sorry I thought you were referring to Church encodings. What system are you considering? Scott encodings are not typeable "naturally" in system F...
cody
CC BY-SA 4.0
2019-05-02T13:41:04.470Z
System F + positive recursive types. Basically the system described in https://pdfs.semanticscholar.org/4200/f8c30ad84a7b4942fda8ae459fad9b52d9dc.pdf.
Labbekak
CC BY-SA 4.0
2019-05-02T17:30:15.893Z
I don't understand what you're expecting as an answer. When you say "is it still possible to analyze recursive calls for termination", what precisely do you mean? If you mean unrestricted resucrive calls, then no. If you mean a restricted form of recursive calls, then what s this restricted form?
Andrej Bauer
CC BY-SA 4.0
2019-05-02T19:51:17.713Z
Yes I mean can we add a restrictive form of recursion (namely well-founded structural recursion) just like the foetus paper does, even if we don't have ADT and case analysis, if we encode ADTs using Scott-encodings.
Labbekak
CC BY-SA 4.0
2019-05-03T20:27:36.610Z
The point of an encoding is that it encodes the thing you want. The meaning of "encode ADT" is to encode the constructors *and* the eliminators (i.e., structural recursion) in a way that gives the expected equations and/or computation rules. So, I still don't understand what you're looking for.
Andrej Bauer
CC BY-SA 4.0
2019-05-04T19:31:25.197Z
The reason I asked this question is because I implemented binary numerals and I could not figure out how to write addition efficiently (https://stackoverflow.com/questions/55772053/addition-for-binary-natural-numbers-using-primitive-recursion/55772685#55772685). It turns out (as far as I know) that I need more than primitive recursion to get an efficient implementation! So Church/Parigot encodings are not enough, I want to be more free in what kind of recursion I use. Your comment makes me wonder if maybe there is an encoding that allows me to implement a more efficient addition algorithm.
Labbekak
<lambda-calculus><type-systems><typed-lambda-calculus><recursion>
Termination checking for Scott-encodings in System F with positive-recursive types
Labbekak
# Termination checking for Scott-encodings in System F with positive-recursive types

(Asked by: username_0 on 2019-05-02)

Is there any research on termination analysis on Scott-encodings in System F with positive-recursive types.
All papers I have found use languages with constructors and case analysis (for example foetus).
But given that we can encode any ADT as pure lambdas, by defining an ADT as it's case analysis function, is it still possible to do termination checking similar to how it is done for ADTs?
For example we can encode the natural numbers as:
type Nat = forall t. t -> (Nat -> t) -> t
zero = \z s -> z
succ n = \z s -> s n

and then define addition like:
add n m = n m (\n' -> succ (add n' m))

Is it still possible to analyze the recursive calls for termination?
I am aware of Church-encodings but I am interested in structural recursion specifically.

**Tags:** lambda-calculus, type-systems, typed-lambda-calculus, recursion
> **Comments:**
> **username_1**: Did you mean `Nat = forall t. t -> (t -> t) -> t` instead? Otherwise you'd need recursive types...  
> **username_1**: Ooops, sorry I thought you were referring to Church encodings. What system are you considering? Scott encodings are not typeable "naturally" in system F...  
> **username_0**: System F + positive recursive types. Basically the system described in https://pdfs.semanticscholar.org/4200/f8c30ad84a7b4942fda8ae459fad9b52d9dc.pdf.  
> **username_2**: I don't understand what you're expecting as an answer. When you say "is it still possible to analyze recursive calls for termination", what precisely do you mean? If you mean unrestricted resucrive calls, then no. If you mean a restricted form of recursive calls, then what s this restricted form?  
> **username_0**: Yes I mean can we add a restrictive form of recursion (namely well-founded structural recursion) just like the foetus paper does, even if we don't have ADT and case analysis, if we encode ADTs using Scott-encodings.  
> **username_2**: The point of an encoding is that it encodes the thing you want. The meaning of "encode ADT" is to encode the constructors *and* the eliminators (i.e., structural recursion) in a way that gives the expected equations and/or computation rules. So, I still don't understand what you're looking for.  
> **username_0**: The reason I asked this question is because I implemented binary numerals and I could not figure out how to write addition efficiently (https://stackoverflow.com/questions/55772053/addition-for-binary-natural-numbers-using-primitive-recursion/55772685#55772685). It turns out (as far as I know) that I need more than primitive recursion to get an efficient implementation! So Church/Parigot encodings are not enough, I want to be more free in what kind of recursion I use. Your comment makes me wonder if maybe there is an encoding that allows me to implement a more efficient addition algorithm.  

---

## 2 answers

### Answer by username_1 on 2019-05-03. Score: 6 | Accepted answer

I'll first point you to Types for the Scott Numerals by Plotkin, Cardelli and Abadi, where they show how to encode Scott numerals in plain old system F. This at least shows that you can write the "natural" recursion principles on Scott numerals, and because they correspond to recursors in this encoding, they are guaranteed to terminate.
However, if you want to work directly with the recursive type formulation, you can apply the classical theory of termination of system F augmented with the theory of positive inductive types, comprehensively treated in Ralph Matthes' dissertation, admittedly a technical read.
I'm not 100% sure those techniques apply here though. I think the recursor you'd get for the Scott encoding would be something like
recNat : forall P. ((forall t. t -> (P -> t) -> t) -> P) -> (Nat -> P)

For fixing ideas I wrote a definition in Haskell which was a bit tedious:
rectNat f n = f $ \z s -> n z (\ n' -> s (recNat f n'))

Of course in a Matthes like system, the recursor is primitive and the Haskell definition is simply the operational semantics of the recursor.
and you would write addition by specializing P to Nat -> Nat and implementing the first argument of recNat by:
\n -> n (\m -> m) (\add_n m -> succ $ add_n m)

which I think works out to the correct addition when applied to the recursor.
If you're really adverse to recursors, you can apply standard termination analysis techniques in system F or Calculus of constructions, see e.g. Abel's dissertation which is a real tour-de-force.

Finally, I must caution you against a strange counter example in the realm of recursion with positive inductive types: consider the type
I = (forall t. (t -> t)) -> I

which is positive, since a fortiori it does not even contain recursive arguments! Then one might be tempted to accept the recursive function:
Y :: I -> I
Y i = i Y i

There is no obvious reason to reject this program, since Y is not being recursively applied to any smaller arguments. However, applying Y to the identity function will loop.
All this to say that there are strange counter-examples when dealing with positive inductive types in impredicative settings. However, Scott encodings with structural recursive functions do not seem to trigger these counter-examples, and I believe that they are handled by the standard theory of termination from the literature.

> **Comments:**
> **username_0**: Thanks a lot! I think "A Polymorphic Lambda-Calculus with Sized Higher-Order Types" might contain what I'm after. The reason I asked this question is because I implemented binary numerals and I could not figure out how to write addition efficiently (https://stackoverflow.com/questions/55772053/addition-for-binary-natural-numbers-using-primitive-recursion/55772685#55772685). It turns out (as far as I know) that I need more than primitive recursion to get an efficient implementation! So Church/Parigot encodings are not enough, I want to be more free in what kind of recursion I use.  
> **username_1**: @Labbekak certainly sized types are quite flexible, but somehow I feel like fast (or at least linear time) addition of binary numbers should be possible with primitive recursion, at least depending on endianness. Might be a good question for cs.stackexchange!  
> **username_0**: Thanks, I'll ask that question on cs.stackexchange, I'm also thinking now that it might be possible. Thanks for your answer!  

---

### Answer by username_3 on 2019-05-07. Score: 4

(Sorry for the blatant self-advertisement that follows!)

In addition to what was already said, you should really check out our recent TOPLAS paper (<https://doi.org/10.1145/3285955>), which deals with extensions of System F with (co)inductive types (among other things). In the first part of the paper we define a strongly-normalizing language that can deal with Scott encoding. In particular, pure $\lambda$-calculus (specialized) fixpoints/recursors/iterators for Scott-encoded datatypes can be defined (and typed) in the system. We actually only give one for natural numbers (which is due to Parigot), but it seems that this should generalize easily to other datatypes. And they compute with the expected complexity as far as I remember. Note that our system also supports "Scott-encoded" codata types. For instance, we are able to type a (strongly-normalizing) coiterator for a form of streams.

On the technical side, quantifiers as well as (co)inductive types are handled using subtyping exclusively, which yields a syntax-directed type system that can be implemented easily. Although type-checking is most certainly undecidable here, type annotations can be used to help the system when it does not succeed in finding a proof directly (in practice, very few annotations seem to be required). To handle (sized) (co)inductive types, we rely on a cyclic (subtyping) proof mechanism. Well-foundedness is checked using a variation of the size-change principle of Lee, Jones and Ben-Amram. (In the later part of the paper, cyclic proofs are also used for typing derivations in order to type a general fixpoint.)

Here are the relevant links:

* <https://doi.org/10.1145/3285955> (paper),
* <https://github.com/rlepigre/subml/> (implementation),
* <https://rlepigre.github.io/subml/> (online interpreter).

**edit:** I forgot to say that our system does not require any of the usual positivity or semi-continuity conditions. Our notion of subtyping is fine-grained enough to reject unwanted examples.

> **Comments:**
> **username_0**: Thanks! Very interesting paper and provides a direct answer to my question :)  

---

