[om] semantics of structure sharing

[Richard Fateman]

google finds 4900 hits for church rosser theorem.
  You may know a lot about math without this particular
topic coming up.

RJF

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
> evaluation.
> 
>>Somehow requiring OM to evaluate random()  more than once
>>goes much further.
>>
>>OM can presumably convey two messages from point A to point B.
>>in lisp...
>>
>>(f (+ (random 10)(random 10))
>>
>>
>>or
>>   ((lambda(x)(f (+ x x))) (random 10))
>>
>>
> Agreed.
> 
>>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.
> James
> 
> 
> 
> --
> 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