[om] semantics of structure sharing
fateman at cs.berkeley.edu
Mon Apr 22 06:07:01 CEST 2002
google finds 4900 hits for church rosser theorem.
You may know a lot about math without this particular
topic coming up.
Jimmy Cerra wrote:
>>>If random is a function, the Church-Rosser theorem says they are equivalent
>>>if they both terminate.)
> What is the Church-Rosser theorem??? I don't think I've studies that high up in
> Mathematics, yet. :)
> Jimmy Cerra
> -----Original Message-----
> From: owner-om at openmath.org [mailto:owner-om at openmath.org] On Behalf Of
> jhd at cs.bath.ac.uk
> Sent: Sunday, April 21, 2002 4:09 PM
> To: om at openmath.org
> Cc: J.H.Davenport at bath.ac.uk
> Subject: Re: [om] semantics of structure sharing
> On Thu, 11 Apr 2002, Richard Fateman wrote:
>>I don't understand this OMA(choice... ) business, but frankly
>>any time an OM utterance evaluates ANYTHING, it seems to me
>>to be overstepping its bounds.
> No - it's merely overstepping the bounds of what OM per se prescribes.
> Many OM systems will evaluate, but may attach different meanings to this
>>Somehow requiring OM to evaluate random() more than once
>>goes much further.
>>OM can presumably convey two messages from point A to point B.
>>(f (+ (random 10)(random 10))
>> ((lambda(x)(f (+ x x))) (random 10))
>>It cannot in either case say what (random 10) means. only
>>the recipient can do that.
> It can say something (though might well not in the case of random!) about
> what it means (as opposed to what the recipient does with it!).
>>And frankly, the recipient can evaluate these in any of several
>>ways, including a way that maps the second utterance to the
>>first, probably doing an injustice to the system uttering
>>the lambda. (But ONLY in the case that random is not a function.
>>If random is a function, the Church-Rosser theorem says they
>>are equivalent if they both terminate.)
> I would argue that this is non-compliance, since the OM clearly stated
> that there was onlyone use of random.
>>Perhaps it would help if OM people were more conversant with
>>functional programming. Apologies for repeating myself..
> Quite a few of us do, Richard.
> om at openmath.org - general discussion on OpenMath
> Post public announcements to om-announce at openmath.org
> Automatic list maintenance software at majordomo at openmath.org
> Mail om-owner at openmath.org for assistance with any problems
om at openmath.org - general discussion on OpenMath
Post public announcements to om-announce at openmath.org
Automatic list maintenance software at majordomo at openmath.org
Mail om-owner at openmath.org for assistance with any problems
More information about the Om