[Om] Multistep "equation" symbol?

Professor James Davenport jhd at cs.bath.ac.uk
Tue May 12 04:38:32 CEST 2009


On Mon, May 11, 2009 10:22 pm, Lars Hellström wrote:
>> The reason I say that is what you have is really a (part of) a proof
>> here,
>> especially when one looks at the annotations.
>
> Indeed, or at least the skeleton of (part of) a proof. In my case the
> annotations would mainly specify which identity is applied and where
> (which is not at all obvious -- especially for derivations that employ
> previously derived rules).
>
>>>   * There are several steps in this thing, yet it constitutes
>>>     a natural unit (in whatever document it is part of).
>> Quite. It is a 'proof' and could be a free-standing Lemma. One might not
>> wish to do so for expositional reasons, but a proof ought to be capable
>> of being a chain of sub-proofs.
>>>   * Not all steps employ the same relation.
>> True, but, and this is the hard part to formalise, they must be
>> "logically compatible".
> Well, I don't see much point in formalising that; it must in the end be
> up to the party who constructs this kind of proof to draw some logical
> conclusion from it. Attempts to construct a syntactic description of
> the cases where this is possible are likely to be futile.
Which is one reason I didn't like the syntactic n-ary relation.
But one wishes such a chain to be such that a "sufficiently clever"
verifier could verify it, and one probably wants some subset of such
prrofs to be verifiable by pretty simple verifiers.

>>> PS: While typing up the example, I noticed that it probably wouldn't be
>>> correct since limit1#tendsto (MathML3-ish?) is defined to be ternary,
>>> requesting a type-of-limit as first argument. While I suppose one could
>>> use a lambda to work around that, I can't help wondering why the limit
>>> type is an argument in the first place; wouldn't an attribution be more
>>> appropriate?
>> I expect because of the 'optionality' of attributes, at least in OM1.
>
> Aha!
Having said which, it would be better to define a symbol rather than keep
generating such lambda-expressions, if this applicatin were to go that
way.

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



More information about the Om mailing list