[opentheory-users] redundant commands

[Ramana Kumar]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20151030/eb77d247/attachment.html>