[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
