[om] Re: [om-a] Draft version of OpenMath 1.1 available

[Professor James Davenport]

On Wed, 23 Oct 2002, Andreas Strotmann wrote:
> On Wed, 23 Oct 2002, David Carlisle wrote:
> > > In particular, why not just make repeated variables ``erroneous'' in the
> > > CLtL sense (undefined, but not an error) instead of this arbitrary rule?
> >
> > I think mainly as this effectively keeps all existing reasonable OM
> > objects valid, and with the same interpretation as before. This seems a
> > good objective for a "point" release. For an OM 2 (or if we'd got it
> > right in OM 1) then maybe error would be a possibility but I didn't want
> > to suggest invalidating such objects in OM 1.1.
> 
> Actually, that's why I suggest "erroneous" instead of "error".  That way,
> applications are not required to catch it, and are allowed to interpret it
> any way they like (from false infer anything at all...).  Applications
> would be *allowed* to catch it as an error, though.
> 
> It's just another way of saying "deprecated".  And I think it is close
> enough to the current status.
> 
In principle, David is probably right. However, I know of no program which 
interprets (in the sense David meant) bindings, so I suspect we are 
discussing how many (bound) angels can dance on the point of a needle. 
Andreas is probably right in practice, and we should go directly to what 
we think: repeated variables are wrong (i.e. erroneous in the CTtL sense 
- I assume Andreas means section 1.2.4).

However, I have just read page 819 of [1]. This attaches a "natural" 
meaning (in the sense of the $\lambda\Lambda_{\cal K}$ calculus) to 
multiple occurrences in a binding. It is unfortunate that they 
use left-most whereas the 1.1 draft uses right-most, but that is merely a 
notational convention. In particular, that interpretation is NOT that of 
the 1.1 (and therefore 1.0) rules. Of course, OpenMath neither requires 
not prohibits the use of the $\lambda\Lambda_{\cal K}$ calculus, so one 
could argue that the OpenMath standard should say that repeated variables 
are unspecified, which CLtL "error" does mean.

James

[1] Ishtiaq,S.S. & Pym,D.J.,
    A Relevant Analysis of Natural Deduction.
    J. Logic Computation 8(1998) pp. 809-838.
--
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