[opentheory-users] article reader for HOL4

[Ramana Kumar]

Articles live in their own abstract world of higher order logic, and the goal
of an article reader is to interpret this abstract world in the reader's world
then follow the instructions in the article to extend it. The reader's world
may already include definitions and theorems that the article's world doesn't
(although if it's the other way around, the reader can't use the article). In
that case when the article defines/proves something, the reader just supplies
its existing constant/theorem.

Here's what I'm thinking the reader type should look like:

val read_article   : TextIO.instream ->
 {input_types   : (string, hol_type list -> hol_type) dict
  input_consts  : (string, hol_type -> term) dict
  assumptions   : thm net
  output_types  : (string,
                    {axiom:thm, args:hol_type list, rep:string, abs:string} ->
                    {rep_abs:thm, abs_rep:thm, rep:term, abs:term})
                  dict
  output_consts : (string, term -> {const:term, def:thm}) dict
  axioms        : (term list * term) -> thm } ->
 Thm.thm list

Explanation of the fields:

(By types I mean type operators, where hol_types are understood as operators
that take no arguments.)

Input types are types the article depends on and doesn't define.  The
input_types field is a map from the article's names for these types to
hol_types.

Input consts are constants the article depends on and doesn't define. The
input_consts field is a map from the article's names for these constants to
constant terms.

Assumptions are theorems about the input types and input consts (only; any
exceptions?) that the article needs to use. The assumptions field is a net of
theorems indexed by their conclusions that provides these theorems.

Output types are types that the article will define. The output_types field is
a map from the article's names for these types to functions. Each of these
function performs an action equivalent to defining the new type; if the
reader's world doesn't already contain the type, the function defines it and
returns some information about it, and if the reader's world already includes
the type, the function just returns the information about the existing type.
Each function is provided the type axiom, a list of arguments for the type in
order, and the desired names of the rep and abs constants. It must return the
rep and abs constants and the type bijection theorems. If the type doesn't
exist in the reader's world, this is straightforward: just make a new type
definition. If the type already exists, the reader might have to do some
renaming (or even define a new equivalent type to get the argument order
right). Passing back abs and rep terms that don't have the desired names is
fine: those names are article world names, so the reader just has to make sure
whenever the article turns a constant with that name into a term, it gets back
the right term.

Output consts are constants that the article will define. The output_consts
field is a map from the article's names for these constants to functions. Each
of these functions performs an action equivalent to defining the new constant.
Each function gets the term the constant should be defined as and must return
the constant and a theorem saying it's equal to that term. If the reader's
world already contains the constant, under an equivalent definition, making
that theorem could require some reader-side proving. As with types, the string
that is the article name and the actual (#1 o dest_const) name of the term can
differ, as long as the article can never tell.

Axioms are theorems about the defined constants that the article needs to use
but doesn't prove. If the reader's world already contained the defined
constants, then it might also already contain these theorems. If the reader's
world did not, then it will need to provide these theorems perhaps by proving
them or by calling make_axiom. The axioms field is a function from the desired
(hypothesis,conclusion) pairs to theorems. It is guaranteed to be called on
pairs only after the constants appearing in those pairs have had their
definition functions called, so there is a chance that the reader could supply
some proof procedures here if it previously actually made new definitions. (The
reading of the article could even involve user interaction to prove the
axioms.)

Am I getting the concepts right now?
How would you make this description more accurate?

On Sun, Jan 9, 2011 at 9:50 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> On Sun, Jan 9, 2011 at 8:43 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> On Sun, Jan 9, 2011 at 7:08 PM, Joe Hurd <joe at gilith.com> wrote:
>>> Hi Ramana,
>>>
>>> Thanks for implementing this: HOL4 is now the first theorem prover
>>> with an article reader!
>>>
>>> I'd like to try it out: how do I run it?
>>
>> At this stage it's going to break on anything interesting you try it on...
>> But the basic method would be:
>>
>> Build the latest svn version of HOL4
>>
>> In a HOL4 session, do:
>>
>> val input = (* article file, e.g. TextIO.openIn("/path/to/file.art") *)
>> val asms = (* net of theorems the article depends on, you can use
>> Opentheory.thmsFromList ls to create this from a list of HOL4 theorems *)
>> val consts = (* dictionary of constants the article depends on, keyed by their
>> name, and represented by functions (hol_type -> term).
>> You can use Opentheory.constsFromList ls,
>> e.g. constsFromList [("=",fn ty => Term.mk_const("=",ty))] *)
>> val types = (* dictionary of types the article depends on, keyed by their
>> names, and represented by functions (hol_type list -> hol-type).
>> You can use Opentheory.typesFromList ls,
>> e.g. typesFromList [("->",fn ls => Type.mk_type("fun",ls))] *)
>> val thms = Opentheory.read_article input {thms=asms,consts=consts,types=types}
>>
>> If all goes well, thms should be bound to a list of theorems proved by
>> the article.
>
> I'm starting to discover that this design may be quite broken...
> articles can depend on assumption expressed using constants and types
> defined by the article - how am I supposed to pass those in as
> theorems to read_article? For example the bool-1.0 package has an
> axiom |- !t. (\x. t x) = t, which is provable in HOL using HOL's
> definition of !, but the package wants that theorem for it's own
> version of ! that it defines itself...
>
> I think I must have fundamentally misunderstood how articles are
> supposed to be used. I guess instead of actually defining new
> constants while reading an article, one should just pass in constants
> that you want to act like the ones the article is going to define, and
> pass in theorems you already know about them for the article's
> axioms..?
>
> What's the difference between an assumption and an axiom?
> opentheory info --summary gives lists of input type operators, input
> constants, assumptions, defined constants, axioms, and theorems.
> My new understanding of how to deal with these is as follows:
> input type operators: existing type operators
> input constants: existing constants
> assumptions: unknown? actually these are probably just theorems about
> the input constants, which can be supplied
> defined constants: existing constants that you want the article to
> provide you more theorems about
> axioms: theorems you need to supply about the defined constants
> theorems: theorems you get by reading the article
>
> Does this make sense?
> I will try reworking my reader to act like this...
>
>>
>>>
>>> Cheers,
>>>
>>> Joe
>>>
>>> On Sun, Jan 9, 2011 at 5:43 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>>>> I have added a preliminary version of an article reader to HOL4
>>>> (hol.sf.net, svn r8839)
>>>>
>>>> Which other proof assistants have readers, by the way? Is there a list
>>>> somewhere?
>>>>
>>>> On Sat, Jan 8, 2011 at 5:54 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>>>>> Does anyone know if there's an article reader for HOL4?
>>>>> Or, in fact, which theorem provers have article readers, and where can
>>>>> they be found?
>>>>> I'm thinking if there is none for HOL4 I should write it, and then put
>>>>> it with the HOL4 sources - or should it come with the opentheory?
>>>>>
>>>>
>>>> _______________________________________________
>>>> opentheory-users mailing list
>>>> opentheory-users at gilith.com
>>>> http://www.gilith.com/opentheory/mailing-list
>>>>
>>>
>>> _______________________________________________
>>> opentheory-users mailing list
>>> opentheory-users at gilith.com
>>> http://www.gilith.com/opentheory/mailing-list
>>>
>>
>