[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 < [email protected]> 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 > > >
