[opentheory-users] redundant commands

[Joe Leslie-Hurd]

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
>