[om] semantics of structure sharing

Jimmy Cerra jimbofc at yahoo.com
Mon Apr 22 05:01:30 CEST 2002


>> 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



More information about the Om mailing list