[opentheory-users] defineTypeOp underspecified? / opentheory be used as a proof verifier

[Ramana Kumar]

On 7 August 2015 at 00:30, Günter Rote <rote at inf.fu-berlin.de> wrote:

> I am trying to write an article reader in python, mainly to
> get an understanding how the steps of a formal proof in HOL look like.
>

Sounds like a good idea.


> My question concerns the definition of *defineTypeOp*
> in the article file format
> http://www.gilith.com/research/opentheory/article.html
>
> Since the new constants *abs* and *rep*
> appear in a term like "(⊦ (λa. abs (rep a)) = λa. a)",
> they must have some type:
>
> I guess the new type operator op with name n has
> type parameters α1 ... αk in this order, and
> the types of rep and abs are
>  rep:: n α1 ... αk -> b
>  abs:: b -> n α1 ... αk (using prefix notation for the type-operator)
> where b is the type of t
> Is that true?
>

That is correct.


> In the definition of *opType*, is it required that
> the length n of the list equals the k with which
> the type-operator "op" has been defined?
>

Kind of true, but not really. Type operators can be constructed by the
virtual machine even if they have not previously been defined in the same
article. In that case, the type operator will be one of the "external type
operators" (i.e., an input) to the resulting theory. (N.B. if you use
*typeOp* to create a type operator with the same name as one created by
*defineTypeOp*, they won't alias each other; i.e., if you want to use the
type defined by *defineTypeOp* you have to use the TypeOp object that it
returns. Some related previous mails on this point:
http://www.gilith.com/opentheory/mailing-list/2011-January/000080.html.)

However, I think if you are using a type operator whose definition is known
and supply the wrong number of arguments, article processing will fail. Joe
can probably confirm and clarify this.


> (Maybe my question is based on a basic misunderstanding:
> Can opentheory be used as a proof verifier?
> I.e. If an article file goes through opentheory without
> errors, does it mean that the listed "theorems" can be
> derived from the "assumptions" (using the OpenTheory derivation rules)?
>

Yes. The opentheory tool can be used to verify that articles obey the
derivation rules of (OpenTheory's variant of) HOL.


> (I have seen talks about proof verification by transforming opentheory to
> dedukti (or rather HOL via opentheory to dedukti) and then verifying the
> proof in dedukti. What would be the point of this if this
> verification is also fine in opentheory?)
>

There are at least two points to make here:

1. Dedukti verifies proofs in a different logical system, lambda pi modulo
rewriting, in which HOL (e.g., OpenTheory) can be embedded. The idea is
that it could be a place where theories from different logics could be
combined. Thus it makes sense to import into Dedukti, even if you trust the
opentheory-checked version is correct, to allow the connection with other
things in Dedukti.

2. It's always good to have multiple implementations of a proof checker,
since proof checkers can contain bugs but the chances of two very different
implementations having the same bugs are low. (To be clear, proof checkers
don't typically have many bugs, but it's possible.) The opentheory tool
wasn't designed primarily as a proof checker (it has other design goals
too), so it's not the smallest and simplest piece of code doing that job,
hence maybe you would prefer to trust an independent, purpose-built
checker. (I don't think Dedukti is that either though.) The CakeML project
(of which I'm a developer) takes the idea of reducing the need to trust the
proof checker to an extreme: we are working on a proof checker whose
machine-code implementation is itself verified to only accept theories that
are true in all (standard) models of higher-order logic. (Verified in the
sense of having a proof in OpenTheory deriving that fact.)


>
> --
> G"unter Rote (Germany=49)30-838-75150 (office)
> Freie Universit"at Berlin
> Institut f"ur Informatik
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150808/7435ed08/attachment.html>