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

Joe Leslie-Hurd joe at gilith.com
Sat Aug 8 01:16:09 UTC 2015


Hi Gunter and Ramana,

>> 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.

Thanks for the clarification, I have added a note to defineConst and
defineTypeOp to spell this out:

http://www.gilith.com/research/opentheory/article.html#defineConstCommand
http://www.gilith.com/research/opentheory/article.html#defineTypeOpCommand

> 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.

I don't believe this affects soundness, so I regard this as
implementation-dependent behaviour. In the opentheory logical kernel
you can use a defined type operator with the wrong number of arguments
or a defined constant outside of its principal type, but there won't
be much you can prove about such types/terms. The logical kernels of
other systems might throw an exception if you try to construct such
types/terms.

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

Agreed, and not just the opentheory tool, but any tool that processes
articles (such as your python tool in development).

Cheers,

Joe



More information about the opentheory-users mailing list