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

Gabriel Scherer gabriel.scherer at gmail.com
Thu May 20 03:17:27 EDT 2021


>
> 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 <jasongross9 at 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.scherer at 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 <jasongross9 at 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 <tringer at 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.krishnaswami at 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-Lö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.krishnaswami at gmail.com
>>> > > > <mailto:neelakantan.krishnaswami at 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 Gö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
>>> > > >      >
>>> > > >
>>> > >
>>> >
>>>
>>


More information about the Types-list mailing list