From: Matt Oliveri <atmacen@gmail.com>
To: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] Re: Why do we need judgmental equality?
Date: Mon, 11 Feb 2019 00:23:02 -0800 (PST) [thread overview]
Message-ID: <be30b081-9400-4333-b5ff-02e6a0ad7076@googlegroups.com> (raw)
In-Reply-To: <2b86e469-309d-4a7a-8ad0-d7a0cb376c74@www.fastmail.com>
[-- Attachment #1.1: Type: text/plain, Size: 6567 bytes --]
On Saturday, February 9, 2019 at 9:44:39 AM UTC-5, Jonathan Sterling wrote:
>
> But this approach is not likely to yield *proof assistants* that are more
> usable than existing systems which have replaced definitional equality with
> propositional equality.
>
> I am referring to Nuprl --
A discussion of the usability of propositional equality would not be
complete without distinguishing equality that's reflective, or at least
"subsumptive", from equality that's merely strict. Subsumptive equality is
when the equality elimination rule rewrites in the type of a term without
changing the term. There are no coercions. The way reflective equality is
implemented in Nuprl is essentially a combination of subsumptive equality
and extensionality principles. In ITT + UIP or Observational TT (OTT),
there's a strict propositional equality, but you still have coercions.
I see the avoidance of coercions as the main practical benefit of Nuprl's
approach.
One's approach to automation of equality checking is somewhat orthogonal,
and I'm less opinionated about that. A number of dependent type systems
exist based on an idea of Aaron Stump to use a combination of some
algorithmic equality, and subsumptive (but non-extensional, non-reflective)
equality. My impression is that Zombie is one such system.
usually Nuprl is characterized as using equality reflection, but this is
> not totally accurate (though there is a sense in which it is true).
To clarify, it depends on what you take to be judgmental equality. If it's
the equality that determines what's well-typed, then Nuprl has equality
reflection. Of course no useful system will implement reflective equality
as an algorithm, since it's infeasible. So any algorithmic equality will be
some other equality judgment. But the "real" judgmental equality is
precisely the equality type. (As you say later.)
When I say "definitional equality" for a formalism, what I mean is that if
> I have a proof object D of a judgment J, if J is definitionally equal to
> J', then D is also already a proof of J'. Definitional equality is the
> silent equality. In most formalisms, definitional equality includes some
> combination of alpha/beta/eta/xi, but in Nuprl is included ONLY alpha.
Interesting. So you're counting Nuprl's proof trees and, say, Agda's terms
as proof objects?
But what about Nuprl's direct computation rules? These allow untyped beta
reduction and expansion anywhere in a goal. This justifies automatic beta
normalization by all tactics. I don't know if Nuprlrs take advantage of
this, but I think they should.
Proof objects must NOT be confused with realizers, of course -- just like
> we do not confuse Coq proofs with the OCaml code that they could be extract
> to.
>
To clarify, the realizers in Nuprl are Nuprl's *terms*. They are what get
normalized; they are what appear in goals. The thing in Coq corresponding
most closely to Nuprl's proof trees are Coq's proof scripts, not terms. The
passage from Nuprl's proofs to terms is called "witness extraction", and is
superficially similar to Coq's program extraction, but its role is
completely different. A distinction between proof objects and terms is
practically necessary to avoid coercions, since you still need to tell the
proof assistant how to use equality *somehow*. In other words, whereas
Coq's proof scripts are an extra, Nuprl's proof engine is primitive.
(Similarly, in Andromeda, the distinction between AML programs and terms is
necessary.)
...the equality type (a judgment whose derivations are crucially taken only
> up to alpha, rather than up to beta/eta/xi).
>
Although you may wish otherwise, Nuprl's judgments all respect
computational equivalence, which includes beta conversion. (This is the
justification of the direct computation rules.)
Nuprl is in essence what it looks like to remove all definitional
> equalities and replace them with internal equalities. The main difference
> between Nuprl and Thorsten's proposal is that Nuprl's underlying objects
> are untyped -- but that is not an essential part of the idea.
>
This doesn't seem right, since Nuprl effectively has untyped beta
conversion as definitional equality. So I would say it *is* essential that
Nuprl is intrinsically untyped. Its untyped definitional equality is all
about the underlying untyped computation system.
The reason I bring this up is that the question of whether such an idea can
> be made usable, namely using a formalism with only alpha equivalence
> regarded silently/definitionally, and all other equations mediated through
> the equality type, can be essentially reduced to the question of whether
> Nuprl is practical and usable, or whether it is possible to implement a
> version of that idea which is practical and usable.
>
This is an interesting comparison. But because I consider Nuprl as having
untyped definitional equality, and a powerful approach to avoiding
coercions, I have to disagree strongly. By your argument, Thorsten's
proposal would be at least as bad as Nuprl. (For practical usability.) But
I think it would probably be much worse, because I think Nuprl is pretty
good. Some of that is because of beta conversion. But avoiding coercions
using subsumptive equality is also really powerful. Thorsten didn't say,
but I'm guessing his proposal wouldn't use that.
(I would really like it if Nuprl could be accurately likened to some other
proposal, since it'd probably get more people thinking about it. Oh well.
The most similar systems to Nuprl, other than its successors, are
Andromeda, with reflective equality, and the Stump lineage I mentioned,
with subsumptive equality. PVS, Mizar, and F* might be similar too.)
The main purpose of this message is not to disagree with you, Jon. I'm
mostly trying to sing the praises of Nuprl, because I feel that you've
badly undersold it.
I don't know what the best way to deal with dependent types is. But I think
avoiding type annotations and coercions while getting extensional equality
is really good. I don't know about avoiding *all* type annotations; maybe
that makes automation too hard. But I suspect the ideal proof assistant
will be more like Nuprl than like Coq or Agda.
--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
[-- Attachment #1.2: Type: text/html, Size: 7914 bytes --]
next prev parent reply other threads:[~2019-02-11 8:23 UTC|newest]
Thread overview: 71+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-01-30 11:54 [HoTT] " Felix Rech
2019-02-05 23:00 ` [HoTT] " Matt Oliveri
2019-02-06 4:13 ` Anders Mörtberg
2019-02-09 11:55 ` Felix Rech
2019-02-16 15:59 ` Thorsten Altenkirch
2019-02-17 1:25 ` Michael Shulman
2019-02-17 7:56 ` Thorsten Altenkirch
2019-02-17 9:14 ` Matt Oliveri
2019-02-17 9:18 ` Michael Shulman
2019-02-17 10:52 ` Thorsten Altenkirch
2019-02-17 11:35 ` streicher
2019-02-17 11:44 ` Thorsten Altenkirch
2019-02-17 14:24 ` Bas Spitters
2019-02-17 19:36 ` Thomas Streicher
2019-02-17 21:41 ` Thorsten Altenkirch
2019-02-17 12:08 ` Matt Oliveri
2019-02-17 12:13 ` Matt Oliveri
2019-02-20 0:22 ` Michael Shulman
2019-02-17 14:22 ` [Agda] " Andreas Abel
2019-02-17 9:05 ` Matt Oliveri
2019-02-17 13:29 ` Nicolai Kraus
2019-02-08 21:19 ` Martín Hötzel Escardó
2019-02-08 23:31 ` Valery Isaev
2019-02-09 1:41 ` Nicolai Kraus
2019-02-09 8:04 ` Valery Isaev
2019-02-09 1:58 ` Jon Sterling
2019-02-09 8:16 ` Valery Isaev
2019-02-09 1:30 ` Nicolai Kraus
2019-02-09 11:38 ` Thomas Streicher
2019-02-09 13:29 ` Thorsten Altenkirch
2019-02-09 13:40 ` Théo Winterhalter
2019-02-09 11:57 ` Felix Rech
2019-02-09 12:39 ` Martín Hötzel Escardó
2019-02-11 6:58 ` Matt Oliveri
2019-02-18 17:37 ` Martín Hötzel Escardó
2019-02-18 19:22 ` Licata, Dan
2019-02-18 20:23 ` Martín Hötzel Escardó
2019-02-09 11:53 ` Felix Rech
2019-02-09 14:04 ` Nicolai Kraus
2019-02-09 14:26 ` Gabriel Scherer
2019-02-09 14:44 ` Jon Sterling
2019-02-09 20:34 ` Michael Shulman
2019-02-11 12:17 ` Matt Oliveri
2019-02-11 13:04 ` Michael Shulman
2019-02-11 15:09 ` Matt Oliveri
2019-02-11 17:20 ` Michael Shulman
2019-02-11 18:17 ` Thorsten Altenkirch
2019-02-11 18:45 ` Alexander Kurz
2019-02-11 22:58 ` Thorsten Altenkirch
2019-02-12 2:09 ` Jacques Carette
2019-02-12 11:03 ` Matt Oliveri
2019-02-12 15:36 ` Thorsten Altenkirch
2019-02-12 15:59 ` Matt Oliveri
2019-02-11 19:27 ` Matt Oliveri
2019-02-11 21:49 ` Michael Shulman
2019-02-12 9:01 ` Matt Oliveri
2019-02-12 17:54 ` Michael Shulman
2019-02-13 6:37 ` Matt Oliveri
2019-02-13 10:01 ` Ansten Mørch Klev
2019-02-11 20:11 ` Matt Oliveri
2019-02-11 8:23 ` Matt Oliveri [this message]
2019-02-11 13:03 ` Jon Sterling
2019-02-11 13:22 ` Matt Oliveri
2019-02-11 13:37 ` Jon Sterling
2019-02-11 6:51 ` Matt Oliveri
2019-02-09 12:30 ` [HoTT] " Thorsten Altenkirch
2019-02-11 7:01 ` Matt Oliveri
2019-02-11 8:04 ` Valery Isaev
2019-02-11 8:28 ` Matt Oliveri
2019-02-11 8:37 ` Matt Oliveri
2019-02-11 9:32 ` Rafaël Bocquet
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=be30b081-9400-4333-b5ff-02e6a0ad7076@googlegroups.com \
--to=atmacen@gmail.com \
--cc=HomotopyTypeTheory@googlegroups.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).