On Mon, March 23, 2009 12:51 pm, David Carlisle wrote: >> Hence I want all 'bindings' in OM to require a 'condition on the bound >> variables'. Syntactically this can, perhaps, be omitted but with an >> assumed default value. > It's perfectly reasonably (but a big change) to want to base things on a > typed (or conditioned) system rather than an untyped one. (Not sure that > OM could survive the surgery required, but it's certainly something that > could be considered). A very good statement. I wonder what the ECC people have to say? > But that seems a more or less completely separate issue from > James/Michael's proposal, which doesn't add a distinguished syntactic > component to OMBind for conditions (such as the once proposed OMC element) > but rather just adds an open ended list of expression terms to be > included in the binding, which may (on a symbol-by-symbol basis) be > taken to be conditions on the bound variable, or constituent subterms > of the expression being bound or anything else. That's true, though the symbol would have to state (via STS, and we haven't discussed the necessary extension to STS) WHETHER it accepted them at all, and the FMP would presumably say something about them, though that's certainly a pretty weak presumption. Another difference is that a 'condition' in JHD/MK, is also rather different from a type. \forall n\in\N (which doesn't need JHD/MK) is pretty learly a type as well as a condition, but (x,y,z)\in ellipsoid ((4) in JHD/MK) is harder to view as a type, though there are type theorists who could.
James Davenport Visiting Full Professor, University of Waterloo Otherwise: Hebron & Medlock Professor of Information Technology and Chairman, Powerful Computing WP, University of Bath OpenMath Content Dictionary Editor and Programme Chair, OpenMath 2009 IMU Committee on Electronic Information and Communication _______________________________________________ Om3 mailing list [email protected] http://openmath.org/mailman/listinfo/om3
