[Om] Mathematical Vernacular in formulae

Peter Horn hornp at mathematik.uni-kassel.de
Wed Jan 26 13:54:54 CET 2011


Hey!

> $\{\langle a,b\rangle\bigl|\text{$a\in T$ and $P$ terminates for $a$ with $b$}\}$

Whenever I advertise OM (and I did that quite some times in the last
couple of years), I tell people that OM is focusing on semantics and
that (normally) all semantics is encoded in OMSs, whereas everything
else is just 'stupid' building blocks.

This is an example where the actual semantics is encoded in
whatever-but-not-an-OMS, so from a formal point of view I'm quite
unhappy. I think introducing a terminates_for symbol is the right way
to go.

It is probably impossible to use one language for both, semantics and markup...

Just my 5 shekel,
    Peter


More information about the Om mailing list