Thread Links Date Links
Thread Prev Thread Next Thread Index Date Prev Date Next Date Index

Re: SUO: Units of measure - representation of multipliers




Adam,

Your solution would indeed work:

AP> But also not a case where such a lattice is required.  A much
simpler
> solution is simply to create a new class of Number which has a precision
> associated with it and an associated function to extract the Number minus
> its precision.  I'll have a more detailed message about that shortly.

Given a lattice of theories, which may reuse the same concept and
relation names, it is always possible to map the entire lattice into
one giant theory by a very simple process:

 1. Assign each theory a unique id, such as th0 for the top,
    and th1, th2, th3, ... for the rest.

 2. Then replace any symbol S in theory THi with THi.S.

 3. Then throw all axioms into one giant pot.

Even though the definition of number in th23211 may be inconsistent
with the definition of number in th865587, there would be no
inconsistency between th23211.number and th865587.number.

What you would lose with this method is the ability to construct
new theories as revisions or extensions of older theories.  If you
wanted to construct a new kind of number that was similar to some
old kind, you would have to retrieve all the axioms for the old kind
of number and make appropriate modifications to them.

John