[om] semantics of structure sharing

[Andreas Strotmann]

On Sun, 21 Apr 2002 jhd at cs.bath.ac.uk wrote:
> 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.

Actually, I was just trying to factor out a concept in most of our
examples that seem to boil down to an application of something like the
axiom of choice (hence the name).  random() in this sense means a choice
from a set of possibilities weighted by probablilities; root(p) means a
choice of one of the roots of polynomial p; [-1,1] was (in one
interpretation) the choice of an unknown "correct" value within this error
range; etc.

"choice" is therefore (and that's the point) not a function, though its
signature would state that it takes a set or distribution or whatnot and
returns one of its elements.  Which one, we don't know.  It's like a wave
function that hasn't collapsed yet, perhaps.

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

Same here.

> > 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!).

I agree with James here.  We *can* say what it *means* (in the
mathematical statistics sense at least, provided we provide the necessary
detailed characterisation of probablility distribution etc.)

For example, to explain my original point, supposing (random 10) is
integer-valued by declaration in a content dictionary in your example, a
mathematician would feel comfortable assuming the argument to f to be even
in the second example, but not the first, and he might thus be able to
prove certain properties of the second expression that do not necessarily
hold for the first.  This does not involve evaluating.  It just involves
feeling comfortable with assuming that (lambda (x) (+ x x)) generally
means roughly the same thing as (lambda (x) (* 2 x)) if you know that x
stands for integers, and you know that + and * are functions.

Now my original point was that even with semantic sharing in the first
example, the mathematician would not necessarily feel entirely convinced
that the same argument would hold, because the shared *meaning* is "a
choice", not "the choice".  But maybe someone can convince me otherwise.

As another example, REDUCE has the concept of ARBINT(n), where n is a
label.  It stands for "an arbitrary integer", so ARBINT(n)\in\Z is true.
Here, ARBINT(n)=ARBINT(m) is reliably true only if n=m. ARBINT() without
a label corresponds to a   (choice setnames::integers), but with it?  I
frankly don't quite know what to say.

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

But of course it isn't, and the theorem doesn't hold, and functional
programming (a camp I've been in for 20+ years now) has to be taken with a
grain of salt, such as not being entirely sure that
evaluation-by-substitution is a useful model under these circumstances.

-- Andreas

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