[opentheory-users] the Unwanted namespace

[Joe Hurd]

Hi Ramana,

I will say that the recent change I made to eliminate "Unwanted.id tm"
terms in general, rather than simple cases, resulted in a performance
degradation that I'm currently investigating.

But this aside, when the the opentheory tool eventually terminated,
did it successfully eliminate all Unwanted.id terms?

Cheers,

Joe

On Fri, Dec 2, 2011 at 11:53 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> OK it wasn't looping - just taking a long time.
>
> On Fri, Dec 2, 2011 at 7:46 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> My lazy list article made use of Unwanted.id but didn't define it.
>> I've been trying to process it with the new opentheory for about 10
>> minutes and it seems like it's either really slow or caught in a loop.
>> I put the article here cam.xrchz.net/ll.art.gz. There's also the
>> original version from two months ago cam.xrchz.net/llist.art.gz, which
>> I don't know why is different.
>>
>> Here's what I'm looking at:
>> % opentheory info --article -o llist.art llist.art
>> WARNING: 38 objects left on the stack by llist.art
>> WARNING: 473,658 objects left in the dictionary by llist.art
>>
>> Some (maybe optional) output indicating status and progress might be nice.
>>
>> On Thu, Dec 1, 2011 at 10:08 PM, Joe Hurd <joe at gilith.com> wrote:
>>> 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
>>>>
>>>
>>> _______________________________________________
>>> 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