[TYPES] What's a program? (Seriously)

Sat May 22 06:28:14 EDT 2021

Le 19/05/2021 à 17:59, Thomas Streicher a écrit :
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> n Wed, May 19, 2021 at 05:26:52PM +0200, Gabriel Scherer wrote:
>> I am not convinced by the example of Jason and Thomas, which suggests that
>> I am missing something.
>>
>> We can interpret the excluded middle in classical abstract machines (for
>> example Curien-Herbelin-family mu-mutilda, or Parigot's earlier classical
>> lambda-calculus), or in presence of control operators (classical abstract
>> machines being nicer syntax for non-delimited continuation operators). If
>> you ask for for a proof of (A \/ not A), you get a "fake" proof of (not A);
>> if you ever manage to build a proof of A and try to use it to get a
>> contradiction using this (not A), it will "cheat" by traveling back in time
>> to your "ask",  and serve you your own proof of A.
>>
>> This gives a computational interpretation of (non-truncated) excluded
>> middle that seems perfectly in line with Talia's notion of "program". Of
>> course, what we don't get that we might expect is a canonicity property: we
>> now have "fake" proofs of (A \/ B) that cannot be distinguished from "real"
>> proofs by normalization alone, you have to interact with them to see where
>> they take you. (Or, if you see those classical programs through a
>> double-negation translation, they aren't really at type (A \/ B), but
>> rather at its double-negation translation, which has weirder normal forms.)
> All these computational interpretations of classical logic are
> actually constructive interpretations of their negative translations.
> This is maybe not so transparent because macros are used. But if you
> consider the cps translation of these macros you again get the negative
> translations.
>
> I know the French school (Krivine in particular) is very fond of these
> macros. But these macros don't add too computational power.
> More generally, all effects can be translated to a purely functional kernel.
>
> Whether one likes these macros or not presumably depends on whether
> one is more CS person or a mathematician. But these preferences don't
> change strength.
>
> Thomas

I believe this applies CS terminology incorrectly. A whole-program 
translation can increase computational expressiveness. This is very 
useful as this lets CS people give us compilers from high-level 
languages to low-level languages. “Macro” in general indeed refers to 
something which does not add computational power. But if call/cc was 
macro-expressible in the lambda calculus, then I expect CS people to be 
the first to notice. A negative translation is a whole-program translation.

The examples were really about the incompatibility of a notion of 
constructive LEM with other, unspecified, hypotheses. A whole-program 
translation lets you ignore features from the target language, whereas a 
macro does not.

Alternatively, if your notion of computational power does not account 
for computational expressiveness, I suspect there are some kind of 
emergent phenomena in your system your notion might miss.

There have been attempts at making the idea of macro-expressiveness and 
comparison of expressive power rigorous, to begin with Felleisen [1] 
which is a transposition at the level of terms of Kleene's notion of 
eliminability at the level of provability.

Le 20/05/2021 à 13:15, Thomas Streicher a écrit :
> One can extract witnesses only for Pi^0_2 sentences. Otherwise
> classical proofs of existential statements don't give you witnesses.
>
> That's part of our conditio humana...
>
(There are sketches of this conservativity result alluded to in this 
thread, which I will not continue here, instead one can refer to a 
textbook, for instance [2, pp. 198-201].)

The interesting part is of course not going to be that different models 
of computation agree on the notion of computable function from N to N (a 
Pi^0_2 sentence), and that they can disagree beyond. This is a basic 
expectation. What is interesting is what it says beyond.

I find one step missing in Gabriel's and other explanations. The “fake” 
or “cheating” proof (in Gabriel's words) is meant to be used at some 
point inside a bigger program of type N, Bool, or any other type one 
expects to enjoy canonicity, in order to get a final value. Which one 
obtains in the end, because canonicity holds for purely positive types 
(Sigma^0_1 formulae). When one extracts a witness for a Pi^0_2 formula, 
there is no restriction on the shape of the proof: it works as well for 
those obtained by composing presumably-non-constructive ones. This 
relies on the “fake” or “cheating” proofs always providing enough 
information to move the argument forward. Which they do. Then, I believe 
that such proofs are not cheating but constructive.

Is it possible to say that one argues less in good faith than the other, 
between the classical player that backtracks on their position, and the 
intuitionistic opponent who demands amounts of evidence up-front 
unnecessary to the computation of the end result?

And so I believe they are certainly all programs of their respective 
types, for some notion of computation, regardless of whether this notion 
can also be explained in terms of a negative translation of this type 
plus a way of running the result of the transformation of a whole 
program (cf. Friedman's trick, or Prop 10.11 in the reference).

  - - -   - - -   - - -   - - -   - - -   - - -   - - -   - - - - - -   
- - -

This situation, it turns out, is very similar to the one proposed in 
Talia's message: a language in which some terms relying on axioms are 
deemed not computing or "mostly computing" (when seen through an 
intuitionistic lens), but in which some other terms still "fully 
compute". But we have additional guarantees that some terms will always 
"fully compute" depending on their type, rather than their shape.

[1] Felleisen, M., “On the expressive power of programming languages” 
<https://doi.org/10.1016/0167-6423(91)90036-W>.

[2] Krivine, J.-L., “Lambda-calculus, types and models”, 
<https://cel.archives-ouvertes.fr/cel-00574575/>.

-- 
Guillaume Munch-Maccagnoni
Researcher at Inria Bretagne Atlantique
Team Gallinette, Nantes