[ 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
