[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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... Thomas On Thu, May 20, 2021 at 09:17:27AM +0200, Gabriel Scherer wrote: > > > > I don't understand how this semantics works; > > > > Some references: > > - on Parigot's lambda-mu calculus > "An algorithmic interpretation of classical natural deduction", Michel > Parigot, 1992 > https://www.cs.ru.nl/~freek/courses/tt-2011/papers/parigot.pdf > > - on the nicer "classical abstract machines": > "The duality of computation", Hugo Herbelin and Pierre-Louis Curien, 2000 > https://hal.inria.fr/inria-00156377/document > > "Classical *F*??, orthogonality and symmetric candidates", Stéphane > Lengrand and Alexandre MIquel, 2008 > http://www.csl.sri.com/users/sgl/Work/Reports/APAL2007.pdf > > "The duality of computation under focus", Pierre-Louis Curien and > Guillaume Munch-Maccagnoni, 2010 > https://arxiv.org/pdf/1006.2283 > > However, if I understand your interpretation correctly, then term1 should > > reduce to 0 but term2 should reduce to 1. > > > > Yes, terms in classical systems can replace the current continuation (and > erase it or duplicate it), so (let _ := term 0 in term 1) is not > necessarily equivalent to (term 1) (if we assume call-by-value reduction, > at least at type Nat, you will get 0 here instead of 1 as you predict). > Computing with excluded middle is "effectful". > > > Another issue is that typechecking requires normalization under binders, > > but normalization under binders seems to invalidate the semantics you > > suggest, because the proof of A might be not be well-scoped in the context > > in which you asked for it. > > > > If we wrote it all down precisely, I think that there would be free > variables (term variables or co-term/continuation blocks) in various places > that "block" some of the computations, no scope escape. We can perfectly > make sense of reduction under binders in classical calculi, although > sometimes there results are surprising because control effects are > surprising. > > (Trivially, it seems like eta-expanding the proof of fake proof of (not A) > > results in invoking the continuation if you try to fully normalize a term.) > > > > Yes, eta-expansion is not necessarily valid in an effectful system. In > general eta-expansion is only possible terms that your reduction strategy > will not evaluate right away. (If you choose the reduction strategy > carefully you can still have nice eta rules for base connectives.) > > I should also mention that classical calculi are hard to mix with dependent > types (just as most systems that are more effectful or more resourceful > than usual intuitionistic logic): it's an open problem with active research > how to provide nice dependently-typed systems that compute with LEM (in the > syntax of those classical abstract machines, or just with control > operators), exploring various tradeoffs. See for example > > "A Classical Sequent Calculus with Dependent Types", Étienne Miquey, 2019 > https://hal.inria.fr/hal-01519929v3/document > > To summarize: in general giving computational interpretations of newer > axioms has a cost, we move to a new programming model with, typically, > weakened program equivalences; and some powerful extension of our logics > may be incompatible with it or less-compatible. In the particular case of > excluded middle, I have the impression that we now have well-trodded > computational interpretations (including just the double-negation > translation). > > On Thu, May 20, 2021 at 3:53 AM Jason Gross <jasongro...@gmail.com> wrote: > > > > 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. > > > > I don't understand how this semantics works; it seems to me that it > > invalidates the normal reduction rules. > > Consider the following: > > Axiom LEM : forall A, A + (A -> False). > > > > Definition term1 > > := match LEM nat as LEM_nat return _ -> match LEM_nat with inl _ => _ | > > _ => _ end with > > | inl v => fun _ => v > > | inr bad => fun f => f bad > > end (fun bad => let _ := bad 0 in bad 1). > > Definition term2 > > := match LEM nat as LEM_nat return _ -> match LEM_nat with inl _ => _ | > > _ => _ end with > > | inl v => fun _ => v > > | inr bad => fun f => f bad > > end (fun bad => bad 1). > > Lemma pf : term1 = term2. Proof. reflexivity. Qed. > > > > However, if I understand your interpretation correctly, then term1 should > > reduce to 0 but term2 should reduce to 1. > > > > Another issue is that typechecking requires normalization under binders, > > but normalization under binders seems to invalidate the semantics you > > suggest, because the proof of A might be not be well-scoped in the context > > in which you asked for it. (Trivially, it seems like eta-expanding the > > proof of fake proof of (not A) results in invoking the continuation if you > > try to fully normalize a term.) > > > > What am I missing/misunderstanding? > > > > Best, > > Jason > > > > > > On Wed, May 19, 2021 at 11:27 AM Gabriel Scherer < > > gabriel.sche...@gmail.com> 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.) > >> > >> > >> > >> > >> On Wed, May 19, 2021 at 5:07 PM Jason Gross <jasongro...@gmail.com> > >> wrote: > >> > >>> [ The Types Forum, > >>> http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > >>> > >>> Non-truncated Excluded Middle (that is, the version that returns an > >>> informative disjunction) cannot have a computational interpretation in > >>> Turing machines, for it would allow you to decide the halting problem. > >>> More generally, some computational complexity theory is done with > >>> reference > >>> to oracles for known-undecidable problems. Additionally, I'd be > >>> suspicious > >>> of a computational interpretation of the consistency of ZFC or PA ---- > >>> would having a computational interpretation of these mean having a type > >>> theory that believes that there are ground terms of type False in the > >>> presence of a contradiction in ZFC? > >>> > >>> On Wed, May 19, 2021, 07:38 Talia Ringer <trin...@cs.washington.edu> > >>> wrote: > >>> > >>> > [ The Types Forum, > >>> http://lists.seas.upenn.edu/mailman/listinfo/types-list > >>> > ] > >>> > > >>> > Somewhat of a complementary question, and proof to the world that I'm > >>> up at > >>> > 330 AM still thinking about this: > >>> > > >>> > Are there interesting or commonly used logical axioms that we know for > >>> sure > >>> > cannot have computational interpretations? > >>> > > >>> > On Wed, May 19, 2021, 3:24 AM Neel Krishnaswami < > >>> > neelakantan.krishnasw...@gmail.com> wrote: > >>> > > >>> > > [ The Types Forum, > >>> > http://lists.seas.upenn.edu/mailman/listinfo/types-list > >>> > > ] > >>> > > > >>> > > Dear Sandro, > >>> > > > >>> > > Yes, you're right -- I didn't answer the question, since I was too > >>> > > taken by the subject line. :) > >>> > > > >>> > > Anyway, I do think that HoTT with a non-reducible univalence axiom is > >>> > > still a programming language, because we can give a computational > >>> > > interpretation to that language: for example, you could follow the > >>> > > strategy of Angiuli, Harper and Wilson's POPL 2017 paper, > >>> > > *Computational Higher-Dimensional Type Theory*. > >>> > > > >>> > > Another, simpler example comes from Martin Escardo's example upthread > >>> > > of basic Martin-Lo??f type theory with the function extensionality > >>> > > axiom. You can give a very simple realizability interpretation to the > >>> > > equality type and extensionality axiom, which lets every compiled > >>> > > program compute. > >>> > > > >>> > > What you lose in both of these cases is not the ability to give a > >>> > > computational model to the language, but rather the ability to > >>> > > identify normal forms and to use an oriented version of the > >>> equational > >>> > > theory of the language as the evaluation mechanism. > >>> > > > >>> > > This is not an overly shocking phenomenon: it occurs even in much > >>> > > simpler languages than dependent type theories. For example, once you > >>> > > add the reference type `ref a` to ML, it is no longer the case that > >>> > > the language has normal forms, because the ref type does not have > >>> > > introduction and elimination rules with beta- and eta- rules. > >>> > > > >>> > > Another way of thinking about this is that often, we *aren't sure* > >>> > > what the equational theory of our language is or should be. This is > >>> > > because we often derive a language by thinking about a particular > >>> > > semantic model, and don't have a clear idea of which equations are > >>> > > properly part of the theory of the language, and which ones are > >>> > > accidental features of the concrete model. > >>> > > > >>> > > For example, in the case of name generation ??? i.e., ref unit ??? our > >>> > > intuitions for which equations hold come from the concrete model of > >>> > > nominal sets. But we don't know which of those equations should hold > >>> > > in all models of name generation, and which are "coincidental" to > >>> > > nominal sets. > >>> > > > >>> > > Another, more practical, example comes from the theory of state. We > >>> > > all have the picture of memory as a big array which is updated by > >>> > > assembly instructions a la the state monad. But this model > >>> incorrectly > >>> > > models the behaviour of memory on modern multicore systems. So a > >>> > > proper theory of state for this case should have fewer equations > >>> > > than what the folk model of state validates. > >>> > > > >>> > > > >>> > > Best, > >>> > > Neel > >>> > > > >>> > > On 19/05/2021 09:03, Sandro Stucki wrote: > >>> > > > Talia: thanks for a thought-provoking question, and thanks everyone > >>> > else > >>> > > > for all the interesting answers so far! > >>> > > > > >>> > > > Neel: I love your explanation and all your examples! > >>> > > > > >>> > > > But you didn't really answer Talia's question, did you? I'd be > >>> curious > >>> > > > to know where and how HoTT without a computation rule for > >>> univalence > >>> > > > would fit into your classification. It would certainly be a > >>> language, > >>> > > > and by your definition it has models (e.g. cubical ones) which, if > >>> I > >>> > > > understand correctly, can be turned into an abstract machine > >>> (either a > >>> > > > rewriting system per your point 4 or whatever the Agda backends > >>> compile > >>> > > > to). So according to your definition of programming language > >>> (point 3), > >>> > > > this version of HoTT would be a programming language simply because > >>> > > > there is, in principle, an abstract machine model for it? Is that > >>> what > >>> > > > you had in mind? > >>> > > > > >>> > > > Cheers > >>> > > > /Sandro > >>> > > > > >>> > > > > >>> > > > On Wed, May 19, 2021 at 6:21 AM Neel Krishnaswami > >>> > > > <neelakantan.krishnasw...@gmail.com > >>> > > > <mailto:neelakantan.krishnasw...@gmail.com>> wrote: > >>> > > > > >>> > > > [ The Types Forum, > >>> > > > http://lists.seas.upenn.edu/mailman/listinfo/types-list > >>> > > > <http://lists.seas.upenn.edu/mailman/listinfo/types-list> ] > >>> > > > > >>> > > > Dear Talia, > >>> > > > > >>> > > > Here's an imprecise but useful way of organising these ideas > >>> that I > >>> > > > found helpful. > >>> > > > > >>> > > > 1. A *language* is a (generalised) algebraic theory. Basically, > >>> > think > >>> > > > of a theory as a set of generators and relations in the > >>> style > >>> > of > >>> > > > abstract algebra. > >>> > > > > >>> > > > You need to beef this up to handle variables (e.g., see > >>> the > >>> > > work of > >>> > > > Fiore and Hamana) but (a) I promised to be imprecise, and > >>> (b) > >>> > > the > >>> > > > core intuition that a language is a set of generators for > >>> > terms, > >>> > > > plus a set of equations these terms satisfy is already > >>> totally > >>> > > > visible in the basic case. > >>> > > > > >>> > > > For example: > >>> > > > > >>> > > > a) the simply-typed lambda calculus > >>> > > > b) regular expressions > >>> > > > c) relational algebra > >>> > > > > >>> > > > 2. A *model* of a a language is literally just any old > >>> mathematical > >>> > > > structure which supports the generators of the language > >>> and > >>> > > > respects the equations. > >>> > > > > >>> > > > For example: > >>> > > > > >>> > > > a) you can model the typed lambda calculus using sets > >>> > > > for types and mathematical functions for terms, > >>> > > > b) you can model regular expressions as denoting > >>> particular > >>> > > > languages (ie, sets of strings) > >>> > > > c) you can model relational algebra expressions as sets of > >>> > > > tuples > >>> > > > > >>> > > > 2. A *model of computation* or *machine model* is basically a > >>> > > > description of an abstract machine that we think can be > >>> > > implemented > >>> > > > with physical hardware, at least in principle. So these > >>> are > >>> > > things > >>> > > > like finite state machines, Turing machines, Petri nets, > >>> > > pushdown > >>> > > > automata, register machines, circuits, and so on. > >>> Basically, > >>> > > think > >>> > > > of models of computation as the things you study in a > >>> > > computability > >>> > > > class. > >>> > > > > >>> > > > The Church-Turing thesis bounds which abstract machines we > >>> > > think it > >>> > > > is possible to physically implement. > >>> > > > > >>> > > > 3. A language is a *programming language* when you can give at > >>> > least > >>> > > > one model of the language using some machine model. > >>> > > > > >>> > > > For example: > >>> > > > > >>> > > > a) the types of the lambda calculus can be viewed as > >>> partial > >>> > > > equivalence relations over Go??del codes for some > >>> universal > >>> > > turing > >>> > > > machine, and the terms of a type can be assigned to > >>> > > equivalence > >>> > > > classes of the corresponding PER. > >>> > > > > >>> > > > b) Regular expressions can be interpreted into finite > >>> state > >>> > > > machines > >>> > > > quotiented by bisimulation. > >>> > > > > >>> > > > c) A set in relational algebra can be realised as > >>> equivalence > >>> > > > classes of B-trees, and relational algebra expressions > >>> as > >>> > > nested > >>> > > > for-loops over them. > >>> > > > > >>> > > > Note that in all three cases we have to quotient the > >>> machine > >>> > > model > >>> > > > by a suitable equivalence relation to preserve the > >>> equations of > >>> > > the > >>> > > > language's theory. > >>> > > > > >>> > > > This quotient is *very* important, and is the source of a > >>> lot > >>> > of > >>> > > > confusion. It hides the equivalences the language theory > >>> wants > >>> > to > >>> > > > deny, but that is not always what the programmer wants ??? > >>> e.g., > >>> > is > >>> > > > merge sort equal to bubble sort? As mathematical functions, > >>> > they > >>> > > > surely are, but if you consider them as operations running > >>> on > >>> > an > >>> > > > actual computer, then we will have strong preferences! > >>> > > > > >>> > > > 4. A common source of confusion arises from the fact that if > >>> you > >>> > have > >>> > > > a nice type-theoretic language (like the STLC), then: > >>> > > > > >>> > > > a) the term model of this theory will be the initial > >>> model in > >>> > > the > >>> > > > category of models, and > >>> > > > b) you can turn the terms into a machine > >>> > > > model by orienting some of the equations the > >>> lambda-theory > >>> > > > satisfies and using them as rewrites. > >>> > > > > >>> > > > As a result we abuse language to talk about the theory of > >>> the > >>> > > > simply-typed calculus as "being" a programming language. > >>> This > >>> > is > >>> > > > also where operational semantics comes from, at least for > >>> > purely > >>> > > > functional languages. > >>> > > > > >>> > > > Best, > >>> > > > Neel > >>> > > > > >>> > > > On 18/05/2021 20:42, Talia Ringer wrote: > >>> > > > > [ The Types Forum, > >>> > > > http://lists.seas.upenn.edu/mailman/listinfo/types-list > >>> > > > <http://lists.seas.upenn.edu/mailman/listinfo/types-list> ] > >>> > > > > > >>> > > > > Hi friends, > >>> > > > > > >>> > > > > I have a strange discussion I'd like to start. Recently I > >>> was > >>> > > > debating with > >>> > > > > someone whether Curry-Howard extends to arbitrary logical > >>> > > > systems---whether > >>> > > > > all proofs are programs in some sense. I argued yes, he > >>> argued > >>> > > > no. But > >>> > > > > after a while of arguing, we realized that we had different > >>> > > > axioms if you > >>> > > > > will modeling what a "program" is. Is any term that can be > >>> typed > >>> > > > a program? > >>> > > > > I assumed yes, he assumed no. > >>> > > > > > >>> > > > > So then I took to Twitter, and I asked the following > >>> questions > >>> > > (some > >>> > > > > informal language here, since audience was Twitter): > >>> > > > > > >>> > > > > 1. If you're working in a language in which not all terms > >>> > compute > >>> > > > (say, > >>> > > > > HoTT without a computational interpretation of univalence, > >>> so > >>> > not > >>> > > > cubical), > >>> > > > > would you still call terms that mostly compute but rely on > >>> > axioms > >>> > > > > "programs"? > >>> > > > > > >>> > > > > 2. If you answered no, would you call a term that does fully > >>> > > > compute in the > >>> > > > > same language a "program"? > >>> > > > > > >>> > > > > People actually really disagreed here; there was nothing > >>> > > resembling > >>> > > > > consensus. Is a term a program if it calls out to an oracle? > >>> > > > Relies on an > >>> > > > > unrealizable axiom? Relies on an axiom that is realizable, > >>> but > >>> > > > not yet > >>> > > > > realized, like univalence before cubical existed? (I suppose > >>> > some > >>> > > > reliance > >>> > > > > on axioms at some point is necessary, which makes this even > >>> > > > weirder to > >>> > > > > me---what makes univalence different to people who do not > >>> view > >>> > > > terms that > >>> > > > > invoke it as an axiom as programs?) > >>> > > > > > >>> > > > > Anyways, it just feels strange to get to the last three > >>> weeks of > >>> > > my > >>> > > > > programming languages PhD, and realize I've never once asked > >>> > what > >>> > > > makes a > >>> > > > > term a program ????. So it'd be interesting to hear your > >>> thoughts. > >>> > > > > > >>> > > > > Talia > >>> > > > > > >>> > > > > >>> > > > >>> > > >>> > >>