Termination checking for Scott-encodings in System F with positive-recursive types 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 -&gt; (Nat -&gt; t) -&gt; t
zero = \z s -&gt; z
succ n = \z s -&gt; s n


and then define addition like:

add n m = n m (\n' -&gt; 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.
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 -&gt; (P -&gt; t) -&gt; t) -&gt; P) -&gt; (Nat -&gt; P)


For fixing ideas I wrote a definition in Haskell which was a bit tedious:

rectNat f n = f $ \z s -&gt; n z (\ n' -&gt; 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 -&gt; Nat and implementing the first argument of recNat by:

\n -&gt; n (\m -&gt; m) (\add_n m -&gt; 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 -&gt; t)) -&gt; 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 -&gt; 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.