[TYPES] What's a program? (Seriously)
Jason Gross
jasongross9 at gmail.com
Wed May 19 21:52:33 EDT 2021
> 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.
I don't understand how this semantics works; it seems to me that it
invalidates the normal reduction rules.
Consider the following:
Axiom LEM : forall A, A + (A -> False).
Definition term1
:= match LEM nat as LEM_nat return _ -> match LEM_nat with inl _ => _ | _
=> _ end with
| inl v => fun _ => v
| inr bad => fun f => f bad
end (fun bad => let _ := bad 0 in bad 1).
Definition term2
:= match LEM nat as LEM_nat return _ -> match LEM_nat with inl _ => _ | _
=> _ end with
| inl v => fun _ => v
| inr bad => fun f => f bad
end (fun bad => bad 1).
Lemma pf : term1 = term2. Proof. reflexivity. Qed.
However, if I understand your interpretation correctly, then term1 should
reduce to 0 but term2 should reduce to 1.
Another issue is that typechecking requires normalization under binders,
but normalization under binders seems to invalidate the semantics you
suggest, because the proof of A might be not be well-scoped in the context
in which you asked for it. (Trivially, it seems like eta-expanding the
proof of fake proof of (not A) results in invoking the continuation if you
try to fully normalize a term.)
What am I missing/misunderstanding?
Best,
Jason
On Wed, May 19, 2021 at 11:27 AM Gabriel Scherer <gabriel.scherer at gmail.com>
wrote:
> 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