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

[Thomas Streicher]

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