What's so great about decidable proof checking?

What's so great about decidable proof checking?

[Matt Oliveri]

[-- Attachment #1.1: Type: text/plain, Size: 1235 bytes --]

Some systems settle for semi-decidable proof checking that's fast in all 
the same cases decidable type checking would've been. Nuprl does this. 
Andromeda seems intended to do this. This is not about ITT vs. ETT or vs. 
Computational TT. (But of course that's how it came up.) It's not about 
intrinsic vs. extrinsic typing. It's not about intuitionistic truth vs. 
derivability. It's just about decidability of formal proof 
checking--considered independently of a particular system--as a "virtue" of 
it's own. Is it, really? I've never heard an argument in its favor. But it 
often seems taken for granted that decidable proof checking is highly 
desirable or even mandatory. Why?

Basic assumptions:
- By "proof", I mean a formal proof on a computer, intended for machine 
checking, not a math paper, not a witness (unless it happens, in some 
system, to be the same thing as a formal proof), not a Brouwerian mental 
construction...
- Proof checking should be reasonably fast in practice.
- We do not trust a proof until it's been fully checked.
- Some decidable proof checking algorithms are algorithmically intractable 
in general, like type checking for MLTT. I am talking, nonetheless, about 
decidability, not tractability.

[-- Attachment #1.2: Type: text/html, Size: 1319 bytes --]

Re: [HoTT] What's so great about decidable proof checking?

[Gabriel Scherer]

We do not trust a proof until it's been fully checked. It also happens
that, for all the different systems you discuss, it is easy to define,
from the trace of a check of a proof, a representation for which
re-checking is decidable -- in ITT it's the proof term, in ETT it's
the derivation *including* equality sub-derivations. If people have
done the work of checking first, they may as well send me the
easy-to-re-check representation; so I consider this decidable version
of the system to be a good representation of valid proofs.

Another way to think of it is that decidability is a good first step
on the way to guaranteed tractability. It's unclear we know how to
give static guarantees that running a general program (or checking a
general proof) will run in a certain complexity, or even better in a
certain number of simple computation steps, in a way that preserves
the ability to conveniently build those proofs. We do have some
reasonable systems that at least guarantee termination, so we may as
well use them. One could conversely argue that there is no reason why
the path to tractable-checking naturally goes through
decidable-checking systems. But it seems a reasonable guess, given
that solving the tractable issue also provides a decidable system, so
the design of a tractable-checking system is included in the space of
decidable-checking system.

(I personally think that arguing too much about these question hits a
point of diminishing return. We are discussing ways to solve a very
hard family of problems, providing mechanically-checkable proofs of
the facts that interest us. If one approach is really better than
others, I would expect it to be easily demonstrated by the fact that
it tackles those very hard problems in a really better way. If the
experience of using one or the other system results in the same
ability to produce mechanically-checkable proofs in practice, then
maybe the design differences did not matter as much as we may think.)

On Tue, Jul 19, 2016 at 10:56 PM, Matt Oliveri <atm...@gmail.com> wrote:
> Some systems settle for semi-decidable proof checking that's fast in all the
> same cases decidable type checking would've been. Nuprl does this. Andromeda
> seems intended to do this. This is not about ITT vs. ETT or vs.
> Computational TT. (But of course that's how it came up.) It's not about
> intrinsic vs. extrinsic typing. It's not about intuitionistic truth vs.
> derivability. It's just about decidability of formal proof
> checking--considered independently of a particular system--as a "virtue" of
> it's own. Is it, really? I've never heard an argument in its favor. But it
> often seems taken for granted that decidable proof checking is highly
> desirable or even mandatory. Why?
>
> Basic assumptions:
> - By "proof", I mean a formal proof on a computer, intended for machine
> checking, not a math paper, not a witness (unless it happens, in some
> system, to be the same thing as a formal proof), not a Brouwerian mental
> construction...
> - Proof checking should be reasonably fast in practice.
> - We do not trust a proof until it's been fully checked.
> - Some decidable proof checking algorithms are algorithmically intractable
> in general, like type checking for MLTT. I am talking, nonetheless, about
> decidability, not tractability.
>
> --
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

Re: [HoTT] What's so great about decidable proof checking?

[Matt Oliveri]

[-- Attachment #1.1: Type: text/plain, Size: 5378 bytes --]

On Wednesday, July 20, 2016 at 2:34:25 AM UTC-4, Gabriel Scherer wrote:
>
> We do not trust a proof until it's been fully checked. It also happens 
> that, for all the different systems you discuss, it is easy to define, 
> from the trace of a check of a proof, a representation for which 
> re-checking is decidable -- in ITT it's the proof term, in ETT it's 
> the derivation *including* equality sub-derivations. If people have 
> done the work of checking first, they may as well send me the 
> easy-to-re-check representation; so I consider this decidable version 
> of the system to be a good representation of valid proofs.
>

A more efficient way to get decidable re-checking is just to tag the proof 
with the number of steps it takes to check it. When re-checking, complain 
as soon as checking takes more steps than promised. Anyway, we agree 
decidable re-checking is easy. Back to whether the initial check should be 
decidable. (Come to think of it, the initial check may well be immediately 
following, or interleaved with proof *search*. And that's not usually 
covered by a decidability guarantee anyway. Seems like another reason not 
to care about decidable checking.)

Another way to think of it is that decidability is a good first step 
> on the way to guaranteed tractability.


I don't agree with this. More on this at the end.

It's unclear we know how to 
> give static guarantees that running a general program (or checking a 
> general proof) will run in a certain complexity, or even better in a 
> certain number of simple computation steps, in a way that preserves 
> the ability to conveniently build those proofs.


Putting a worst-case bound on the complexity of proof checking puts a 
restriction on the convenience of the proof checker. (For checking a 
specific proof, of course you can count how many steps it takes, and if the 
proof assistant does that for you, it seems pretty convenient. But a 
concrete number of steps for a concrete proof isn't saying anything about 
whether proof checking is tractable in general.)

We do have some 
> reasonable systems that at least guarantee termination, so we may as 
> well use them. One could conversely argue that there is no reason why 
> the path to tractable-checking naturally goes through 
> decidable-checking systems. But it seems a reasonable guess, given 
> that solving the tractable issue also provides a decidable system, so 
> the design of a tractable-checking system is included in the space of 
> decidable-checking system.
>

Well that's for sure. I'm basically asking why are we even trying to have 
decidable proof checking. I have no problem with systems where proof 
checking is naturally decidable. What I don't want is for undecidable proof 
checking to count against a system.

(I personally think that arguing too much about these question hits a 
> point of diminishing return. We are discussing ways to solve a very 
> hard family of problems, providing mechanically-checkable proofs of 
> the facts that interest us. If one approach is really better than 
> others, I would expect it to be easily demonstrated by the fact that 
> it tackles those very hard problems in a really better way. If the 
> experience of using one or the other system results in the same 
> ability to produce mechanically-checkable proofs in practice, then 
> maybe the design differences did not matter as much as we may think.)
>

Currently, as far as I know, there is no pair of proof assistants whose 
only significant difference is whether proof checking is decidable. If our 
community wanted to try and do this really scientifically, we could make 
two superficially similar systems, one for OTT, and one for ETT. But even 
then I'm not convinced the relative success of the systems could be 
attributed to their remaining technical differences.

I'm not discussing this in the abstract to try to reach a shared opinion of 
which style of proof checking is better. I'm discussing it to find out why 
"type checking is undecidable" is ever considered a serious disadvantage of 
e.g. ETT. Specifically, I want to know why decidable proof checking is even 
a goal, once we already have fast proof checking in practice. Decidable 
checking is neither necessary nor sufficient for fast proof checking in 
practice. It's necessary, but nowhere near sufficient, for worst-case 
tractable checking.

Type checking MLTT is intractable because it involves structural recursion. 
In other words, reducing the judgmental beta rules for inductive types. 
More generally, the idea that the type checker should be able to perform 
the computations defined in the type theory seems to mean that the type 
checker's complexity is at least as high as that of any definable function. 
And even quite weak type theories can define marvelously-complex functions.

But I'm not against computationally rich (and therefore worst-case 
intractable) type/proof checking. I'm all for it. Indeed, I'm basically 
asking why we would want to stop short of Turing-complete proof checking, 
by wishing for it to be decidable.

I think de Bruijn cautioned against complex type checkers. I think the 
AUTOMATHs all had efficient checking. So you had to hand-crank all the 
interesting equations. I assumed it was deliberate that recent proof 
assistants for dependent type theories have intractable type checking.

[-- Attachment #1.2: Type: text/html, Size: 6257 bytes --]

Re: [HoTT] What's so great about decidable proof checking?

[Jon Sterling]

On Wed, Jul 20, 2016, at 02:12 AM, Matt Oliveri wrote:
> On Wednesday, July 20, 2016 at 2:34:25 AM UTC-4, Gabriel Scherer wrote:
> >
> > We do not trust a proof until it's been fully checked. It also happens 
> > that, for all the different systems you discuss, it is easy to define, 
> > from the trace of a check of a proof, a representation for which 
> > re-checking is decidable -- in ITT it's the proof term, in ETT it's 
> > the derivation *including* equality sub-derivations. If people have 
> > done the work of checking first, they may as well send me the 
> > easy-to-re-check representation; so I consider this decidable version 
> > of the system to be a good representation of valid proofs.
> >
> 
> A more efficient way to get decidable re-checking is just to tag the
> proof 
> with the number of steps it takes to check it. When re-checking, complain 
> as soon as checking takes more steps than promised. Anyway, we agree 
> decidable re-checking is easy. Back to whether the initial check should
> be 
> decidable. (Come to think of it, the initial check may well be
> immediately 
> following, or interleaved with proof *search*. And that's not usually 
> covered by a decidability guarantee anyway. Seems like another reason not 
> to care about decidable checking.)
> 
> Another way to think of it is that decidability is a good first step 
> > on the way to guaranteed tractability.
> 
> 
> I don't agree with this. More on this at the end.
> 
> It's unclear we know how to 
> > give static guarantees that running a general program (or checking a 
> > general proof) will run in a certain complexity, or even better in a 
> > certain number of simple computation steps, in a way that preserves 
> > the ability to conveniently build those proofs.
> 
> 
> Putting a worst-case bound on the complexity of proof checking puts a 
> restriction on the convenience of the proof checker. (For checking a 
> specific proof, of course you can count how many steps it takes, and if
> the 
> proof assistant does that for you, it seems pretty convenient. But a 
> concrete number of steps for a concrete proof isn't saying anything about 
> whether proof checking is tractable in general.)
> 
> We do have some 
> > reasonable systems that at least guarantee termination, so we may as 
> > well use them. One could conversely argue that there is no reason why 
> > the path to tractable-checking naturally goes through 
> > decidable-checking systems. But it seems a reasonable guess, given 
> > that solving the tractable issue also provides a decidable system, so 
> > the design of a tractable-checking system is included in the space of 
> > decidable-checking system.
> >
> 
> Well that's for sure. I'm basically asking why are we even trying to have 
> decidable proof checking. I have no problem with systems where proof 
> checking is naturally decidable. What I don't want is for undecidable
> proof 
> checking to count against a system.
> 
> (I personally think that arguing too much about these question hits a 
> > point of diminishing return. We are discussing ways to solve a very 
> > hard family of problems, providing mechanically-checkable proofs of 
> > the facts that interest us. If one approach is really better than 
> > others, I would expect it to be easily demonstrated by the fact that 
> > it tackles those very hard problems in a really better way. If the 
> > experience of using one or the other system results in the same 
> > ability to produce mechanically-checkable proofs in practice, then 
> > maybe the design differences did not matter as much as we may think.)
> >
> 
> Currently, as far as I know, there is no pair of proof assistants whose 
> only significant difference is whether proof checking is decidable. If
> our 
> community wanted to try and do this really scientifically, we could make 
> two superficially similar systems, one for OTT, and one for ETT. But even 
> then I'm not convinced the relative success of the systems could be 
> attributed to their remaining technical differences.
> 
> I'm not discussing this in the abstract to try to reach a shared opinion
> of 
> which style of proof checking is better. I'm discussing it to find out
> why 
> "type checking is undecidable" is ever considered a serious disadvantage
> of 
> e.g. ETT. Specifically, I want to know why decidable proof checking is
> even 
> a goal, once we already have fast proof checking in practice. Decidable 
> checking is neither necessary nor sufficient for fast proof checking in 
> practice. It's necessary, but nowhere near sufficient, for worst-case 
> tractable checking.

I don't have much to say about this, since you've said most of what I
would have said already, but let me just suggest that decidability of
proof checking seems to be significant in only one of two (related)
ways:

1. A matter of philosophy: a formal proof "ought to" be decidably
checkable.
2. A matter of definition: if it is not decidably checkable, it is not a
formal proof!

As far as actual practice is concerned, experience with Nuprl, MetaPRL,
JonPRL and RedPRL suggests that decidability is completely irrelevant.
It makes no difference at all in the actual use of a tool, since we can
still make Coq choke on a gigantic term quite easily. (Some of my
acquaintances who work on very gnarly "real world" / practical proofs in
Coq have told me that this is quite routine, and you must be very
cautious in your Coq coding style to avoid it.)

I don't want to get into it, but "trust" seems to me to be a largely
metaphysical issue which is often brought up in verification circles,
but rarely has the significance attributed to it. In the end, we must
come to decide for ourselves whether a particular proof-or-construction
system does what we intend it to do.


> 
> Type checking MLTT is intractable because it involves structural
> recursion. 
> In other words, reducing the judgmental beta rules for inductive types. 
> More generally, the idea that the type checker should be able to perform 
> the computations defined in the type theory seems to mean that the type 
> checker's complexity is at least as high as that of any definable
> function. 
> And even quite weak type theories can define marvelously-complex
> functions.
> 
> But I'm not against computationally rich (and therefore worst-case 
> intractable) type/proof checking. I'm all for it. Indeed, I'm basically 
> asking why we would want to stop short of Turing-complete proof checking, 
> by wishing for it to be decidable.

My perspective is slightly different, but it may be a mere matter of
wording / definition. To me, it's not "proof checking" at all unless
it's decidable (and tractability is completely irrelevant to me, but I
can see why others would be interested in it!). Semidecidable proof
systems are very interesting to me, but I would not consider the
activity to be "proof checking". Rather, I see it as an incremental,
ephemeral process of proof *construction*, which you may terminate at
any time, or speculatively proceed further. There is no problem with the
possible non-wellfoundedness of this procedure, since we will only
observe a finite prefix of it.

Let me say one more thing: Nuprl's refinement logic *does* have a
decidable proof theory. The "semidecidable" tactic system is a
convenient means to produce terms in that proof theory, but that does
not make it definitive. (Obviously, Nuprl's proof theory is not
definitive either, since it is just a means of accessing the meaning
explanation.) But there is absolutely a decidable, formal layer that we
can talk about.

> 
> I think de Bruijn cautioned against complex type checkers. I think the 
> AUTOMATHs all had efficient checking. So you had to hand-crank all the 
> interesting equations. I assumed it was deliberate that recent proof 
> assistants for dependent type theories have intractable type checking.
> 



Kind regards,
Jon

> -- 
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

Re: [HoTT] What's so great about decidable proof checking?

[Matt Oliveri]

[-- Attachment #1.1: Type: text/plain, Size: 2208 bytes --]

Hi, Jon.

On Wednesday, July 20, 2016 at 11:53:45 AM UTC-4, Jonathan Sterling wrote:
>
>
> > 
> > Type checking MLTT is intractable because it involves structural 
> > recursion. 
> > In other words, reducing the judgmental beta rules for inductive types. 
> > More generally, the idea that the type checker should be able to perform 
> > the computations defined in the type theory seems to mean that the type 
> > checker's complexity is at least as high as that of any definable 
> > function. 
> > And even quite weak type theories can define marvelously-complex 
> > functions. 
> > 
> > But I'm not against computationally rich (and therefore worst-case 
> > intractable) type/proof checking. I'm all for it. Indeed, I'm basically 
> > asking why we would want to stop short of Turing-complete proof 
> checking, 
> > by wishing for it to be decidable. 
>
> My perspective is slightly different, but it may be a mere matter of 
> wording / definition. To me, it's not "proof checking" at all unless 
> it's decidable (and tractability is completely irrelevant to me, but I 
> can see why others would be interested in it!). Semidecidable proof 
> systems are very interesting to me, but I would not consider the 
> activity to be "proof checking". Rather, I see it as an incremental, 
> ephemeral process of proof *construction*, which you may terminate at 
> any time, or speculatively proceed further. There is no problem with the 
> possible non-wellfoundedness of this procedure, since we will only 
> observe a finite prefix of it.
>

That seems reasonable. Your distinction between proof construction and 
proof checking seems related to my distinction between proof checking and 
proof re-checking. I guess I'm assuming that proof construction is the only 
part normal users interact with, so I completely de-emphasize what you call 
proof checking.

So I guess you don't consider tactics to be proofs? Just proof constructors?

I know you're OK with systems like ETT and CTT. My question is aimed mainly 
at the staunch proponents of systems like ITT and OTT. (This thread was 
prompted by a comment of Andrew Polonsky, on his recent thread, so I was 
hoping to hear his opinion, for example.)

[-- Attachment #1.2: Type: text/html, Size: 2520 bytes --]