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

Nicolai Kraus nicolai.kraus at gmail.com
Thu May 20 04:00:11 EDT 2021


On Wed, May 19, 2021 at 4:06 PM Jason Gross <jasongross9 at gmail.com> wrote:

> 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.
>

For what it's worth, I don't think you need to add "non-truncated" in the
sentence above. From "truncated" excluded middle, you equally directly
either get a number n such that your program holds after n steps, or you
get that it does not halt at all.

Interesting discussion!
-- Nicolai



> 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