larch idiom for definitions: "converts" [was: rdf as a base]

pat hayes wrote:
> somebody wrote:
>      Could you elucidate the distinction between definitions and assertions, and explain how this differs from ground-fact/rule?
> 
> Ah, now I have painted myself into a corner, since I never fully understood the definition/assertion distinction myself, though it seemed central to many folk (and still does). Although to be fair, the idea of a definition is a pretty common one in mathematics and life generally, in spite of its having no obvious logical content.

There's an interesting formalization/implementation of it in
the larch toolset: in larch, you can say that some operator
in a trait is completely defined in terms of other operators
in the trait. In the syntax, you say

	converts sugar

ala "this trait converts the operator 'sugar' to other terms".

The tools generate proof obligations to prove that if sugar were
renamed, it wouldn't make any difference. For technical
details, see
  http://www.w3.org/XML/9711theory/#about-larch
esp
  2.12 How and when should I use a converts clause?
  http://www.cs.iastate.edu/~leavens/larch-faq.html#SEC28

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/

Received on Thursday, 7 June 2001 13:37:07 UTC