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

[Ansten Mørch Klev]

Dear Talia,


It might be worth remembering that, in discussions of Curry--Howard, the
terms "proof" and "programme" have meanings that (at least at first sight)
do not quite agree with their meaning in other parts of logic and computer
science.


A proof in the Curry--Howard sense may also be called a verifier or a
truth-maker, for it is what makes a proposition true, where truth of a
proposition is understood as the inhabitation of a type. A proof in this
sense is therefore a kind of object, and not an act by means of which you
get to know that a proposition is true. Martin-Löf and others prefer to
call the latter a demonstration. Within type theory, you demonstrate that a
proposition is true by constructing a proof of it, where a proof is thus a
certain term in the language of the theory in question.


A term is called a programme, I take it, by virtue of its being possible to
evaluate it. This is *not* the notion of programme that is assumed in the
phrase "Turing machine programme", since a Turing machine programme is not
itself evaluated. For instance, the term 2+2 is a programme in the sense
that it can be evaluated---to ssss(0), say---but it is clearly not a Turing
machine programme. In the world of Turing machines, the term 2+2 qua
programme rather corresponds to a machine with suitable input on the tape
(two sequences of two 1's in this case).


If we stick to the idea that a term is a programme in the sense that it can
be evaluated, then no higher-order term is a programme. In a higher-order
language, the term +  in isolation may be a term, but it is not by itself
evaluable, just as a Turing machine programme that computes addition is not
by itself evaluable. Rather, in accordance with the type of the term +, you
must complete it with two arguments of type N to get something evaluable.
One can make the same argument with respect to open terms, since an open
term is (or stands for) a function, just as a higher-order term is (or
does). The open term x+y, for instance, is not by itself evaluable. To get
something evaluable, you need to assign values to the variables, yielding
for instance 2+2.


With kind regards,

Ansten Klev

On Wed, May 19, 2021 at 6:21 AM Neel Krishnaswami <
neelakantan.krishnaswami at gmail.com> wrote:

> [ The Types Forum, 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 ]
> >
> > 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
> >
>