
Re: Formal Proof Language Example  HumanReadable?
Posted:
Jun 24, 2009 11:51 AM


On Jun 23, 8:37 pm, slawekk <skoko...@yahoo.com> wrote: > 4. Should support some notion of context to be able to limit the scope > of introduced notation, independent of the defined notions. For > example you should be able to talk about groups using both > multiplicative and additive notation (in different contexts), or use > the same \cdot symbol to denote both general group operation and > multiplication of real numbers (again in different contexts). How > important this need is becomes obvious only when you reach certain > scale.
In this example the NaturalNumbers set (which is imported from edu.mit.natural_number) introduces meaning to the various functions:
x^y x + y x = y x, y are_relative_prime x is odd x <= y x  y 2 x * y
where x and y are NaturalNumbers.
This mechanism functions in the same way as overload resolution does in C++  and when you think about it  this is the same way humans infer what a function means. If I say:
<some_operand_a> <some_operator> <some_operand_b>
Then you mentally search all the known operators that look like "some_operator" to the type of thing that "some_operand_a" and "some_operand_b" represent. There can however be multiple different operators that look exactly like some_operator. Andrew.

