[opentheory-users] redundant commands

[Joe Leslie-Hurd]

That's a good simple optimization.

Another one I discovered in HOL Light is that if you're caching
exported theorems then you automatically take care of such redundant
inferences as

TRANS ( |- x = y) (REFL y)

because the later theorem will match the earlier exported one.

If you discover anything else like this please let the list know: I'm
always interested in techniques that result in smaller articles.

Cheers,

Joe


On Thu, Oct 29, 2015 at 11:26 PM, Ramana Kumar <ramana at member.fsf.org> wrote:
> It would be helpful, but I don't think it's urgent.
>
> I have made the HOL4 writer detect when a call to defineConstList could be
> done via defineConst, and use that instead.
>
> On 30 October 2015 at 14:52, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>
>> Hi Ramana,
>>
>> Version 5 of the article standard comprises a non-redundant set of
>> commands (as far as I know), so one way of achieving your goal is to
>> downgrade a version 6 article to version 5 as follows:
>>
>> opentheory info --article -o output5.art --output-version 5 input.art
>>
>> This also converts the version 6 defineTypeOp command into the
>> incompatible version 5 defineTypeOp command, so it's exactly what you
>> asked for. Also, the inverse transformation from version 5 articles to
>> version 6:
>>
>> opentheory info --article -o output6.art --output-version 6 input.art
>>
>> is rather simple-minded and doesn't implement the cool pattern
>> recognition to create version 6 derived commands from the
>> non-redundant set of version 5 commands.
>>
>> To help developers using the article format, I had been thinking of
>> adding recipes to the description of the redundant version 6 commands
>> in the article standard showing how to implement them in terms of the
>> non-redundant commands, but I never got around to it. Do you think
>> that would be helpful?
>>
>> Cheers,
>>
>> Joe
>>
>> On Thu, Oct 29, 2015 at 4:25 PM, Ramana Kumar <ramana at member.fsf.org>
>> wrote:
>> > (Also, my simulation of defineConst was totally wrong, but I think you
>> > get
>> > the idea. It just needs to use typeOf(t) in more places, and make the
>> > variable twice.)
>> >
>> > On 30 October 2015 at 10:23, Ramana Kumar <ramana at member.fsf.org> wrote:
>> >>
>> >> Even cooler would be to go in the other direction :)
>> >> (I mean see an article snippet that looks like it's doing defineConst
>> >> or
>> >> trans or something, in terms of more primitive commands, and turn it
>> >> into a
>> >> call to the derived command instead.)
>> >>
>> >> On 30 October 2015 at 10:08, Ramana Kumar <ramana at member.fsf.org>
>> >> wrote:
>> >>>
>> >>> I was originally going to suggesting retiring defineConst, but I have
>> >>> realised that what I'm really asking is about redundant commands.
>> >>>
>> >>> The defineConst command is subsumed by the defineConstList command.
>> >>>
>> >>> Unfortunately, I can't write an implementation of defineConst purely
>> >>> in
>> >>> terms of other article commands, because the virtual machine provides
>> >>> no
>> >>> mechanism for retrieving the type of a term, or for keeping track of
>> >>> available keys in the dictionary. However, any article writer will be
>> >>> able
>> >>> to do these things.
>> >>>
>> >>> Then simulating a defineConst command is as easy as doing
>> >>>
>> >>> defineConstList(assume(mk_eq(varTerm(var n),t)),cons n nil)
>> >>>
>> >>> where mk_eq corresponds to making an equality between two terms, and n
>> >>> and t correspond to the arguments to defineConst.
>> >>>
>> >>> I guess there are already redundant commands in the virtual machine,
>> >>> though (like trans).
>> >>>
>> >>> I guess it would be nice (to readers) if there were some switches in
>> >>> the
>> >>> opentheory tool to produce an article with certain redundant commands
>> >>> expanded out into a minimal non-redundant core set of commands.
>> >>
>> >>
>> >
>> >
>> > _______________________________________________
>> > 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
>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>