Termination checking for Scott-encodings in System F with positive-recursive types

Question

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.

Answer 1

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.

Answer 2

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