7
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Did you mean Nat = forall t. t -> (t -> t) -> t instead? Otherwise you'd need recursive types... $\endgroup$ – cody May 2 at 13:09
  • $\begingroup$ Ooops, sorry I thought you were referring to Church encodings. What system are you considering? Scott encodings are not typeable "naturally" in system F... $\endgroup$ – cody May 2 at 13:11
  • $\begingroup$ System F + positive recursive types. Basically the system described in pdfs.semanticscholar.org/4200/…. $\endgroup$ – Labbekak May 2 at 13:41
  • 1
    $\begingroup$ 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? $\endgroup$ – Andrej Bauer May 2 at 17:30
  • 1
    $\begingroup$ 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. $\endgroup$ – Labbekak May 2 at 19:51
6
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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 (stackoverflow.com/questions/55772053/…). 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. $\endgroup$ – Labbekak May 4 at 19:27
  • $\begingroup$ @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! $\endgroup$ – cody May 5 at 15:26
  • $\begingroup$ Thanks, I'll ask that question on cs.stackexchange, I'm also thinking now that it might be possible. Thanks for your answer! $\endgroup$ – Labbekak May 5 at 18:33
3
$\begingroup$

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

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.

$\endgroup$
  • $\begingroup$ Thanks! Very interesting paper and provides a direct answer to my question :) $\endgroup$ – Labbekak May 7 at 14:01

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.