[Om] OM->OM Phrasebook

[Bryce L Nordgren]

-----Paul Libbrecht <paul at activemath.org> wrote: -----

>well, sure... that would be the function of an OM->OM-phrasebook.
>But I think that what you are looking for is a document-format trying
>to encode "food for such a phrasebook", right?
>In our case I suppose it could just mean, maybe, to use FMPs of CDs
>with particular "heads" (i.e. "proposed-implementation").

I really think it's an abuse of the FMPs to use it for this purpose.  These
are not mathematical properties we're bestowing, they're phrasebook
entries.  ALL FMP's must be satisfied.  We want the user (or the app) to
choose only one phrasebook entry.  If FMP is still to stand for Formal
Mathematical Property it really cannot contain this new functionality.

I do agree with everything else you said, however.  The phrasebook entry
could well be provided with the symbol definition, and there could be
multiple phrasebook entries associated with each symbol.  Each phrasebook
entry would contain one and only one <OMOBJ/>.  Alternatively, another file
format could be defined to perform the association (much like the signature
file).  Or both, for that matter.

>the phrasebook, to my knowledge, is the piece of software that would
>be able to do that, right?

I would envision the phrasebook to be the software which essentially
substitutes the phrasebook entry for the symbol wherever the symbol is
encountered...I think that's what the standard intends a phrasebook to be.

I would not try to specify how the phrasebook selects from the options
available to it.  You may even have multiple phrasebooks competing to
handle the same symbol (e.g., if a host app has coded an implementation in
C/C++ for a symbol which also has an OM expression defined.)  Figuring out
which implementation to use is the application's problem.  It may even
allow the user to select an implementation on a case by case basis.

Bryce