[TYPES] What's a program? (Seriously)
Gabriel Scherer
gabriel.scherer at gmail.com
Wed May 19 11:26:52 EDT 2021
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