[opentheory-users] the Unwanted namespace

[Joe Hurd]

Hi Ramana,

I just released a version of the opentheory tool that should eliminate
any occurrences of

Unwanted.id <term>

I wanted to test it on the article that you uploaded some time ago,
but unfortunately the new scheme requires that the Unwanted.id
constants to be eliminated are input constants (i.e., not defined by
the theory).

Could you either (i) upload a new version of your article without the
definition of Unwanted.id or (ii) try the new version of the
opentheory tool yourself to see whether it does the right thing?

Cheers,

Joe

On Mon, Oct 10, 2011 at 12:55 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> Unfortunately I can see other ways that terms like these could enter
>> the state, such as
>>
>> appThm (|- (\f. f x) = t) (|- Unwanted.id = u)
>>
>> followed by betaConv of the LHS at a later point.
>
> So we would need to consider betaConv too...
> Anything else?
>
>> I'd really like a scheme that eliminates all occurrences of the
>> Unwanted.id constant from a proof, if that was possible. And by this I
>> mean that grepping the resulting article for occurrences of the
>> "Unwanted" namespace will not turn up any results.
>
> OK.
>
> I think your current treatment of appTerm is fine - it won't fail, and
> it removes those occurrences of Unwanted.id from the article file.
>
> So let's consider appThm and betaConv.
> These are the general forms I see introducing unwanted terms:
>
> appThm (|- Unwanted.id = f) (|- x = y)
> appThm (|- f = Unwanted.id) (|- x = y)
> betaConv (|- (\f. t[f x]) Unwanted.id)
>
> What happens if you just change the semantics of all of these commands
> to replace any resulting (Unwanted.id t) terms by (t), and also
> prevent Unwanted.id from being defined (to stop an obvious soundness
> problem)?
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>