[om] a couple of questions

[Andrew Solomon]

Ok, so I propose introducing a new cd "fns2" with
a single symbol to start with (name="constant")
and the following expresses the tautology "a \in {a,b}".

How does that sound?

Andrew


<OMOBJ>
 <OMBIND>
	 <OMS cd="fns2" name="constant"/>
	 <OMBVAR>
		 <OMV name="a"/>
		 <OMV name="b"/>
	 </OMBVAR>
	 <OMA>
		 <OMS cd="set1" name="in"/>
		 <OMV name="a"/>
		 <OMA>
			 <OMS cd="set1" name="set"/>
			 <OMV name="a"/>
			 <OMV name="b"/>
		 </OMA>
	 </OMA>
 </OMBIND>
</OMOBJ>
On Tue, Apr 17, 2001 at 07:25:13AM -0700, Stephen Braham wrote:
> 
> 
> Steve Linton wrote:
> > 
> > The nicest solution perhaps would be to define a binding constructor for
> > defining a finite set of bound variables. Then you could create a scope in
> > which a, b, and c where the bound variables of this constructor, and even
> > non-CD reading applications would know that only the names of a b and c were
> > meaningful, and how far that meaning extended.
> > 
> >         steve
> 
> I'd go even stronger and say this is the ONLY way to do things. For
> the semantic meaning to be preserved, there must be a corresponding
> Lambda construction to isolate the defining variables.
> 
> Just as OMSTR is a cheat, so can using OMV's on their own be a cheat.
> Generally, if the OMV isn't going to be referred to in an external
> statement, it generally should be bound.
> 
> Indeed, I'd say that's why we decided to have bindings explicit in the
> language!
> 
> 				Steve
> 
> --
> Stephen P. Braham			Director, PolyLAB
> warp at polylab.sfu.ca			TIME Centre 
> (604) 268-7981				Simon Fraser University 
> (fax) 268-7980				Harbour Centre Campus
> http://team.polylab.sfu.ca/~warp/	Vancouver, BC, Canada
> 
>    PolyLAB: From the Classroom to Space, http://polylab.sfu.ca/
> 

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