next up previous
Next: node13.html Up: An Introduction to the Previous: Soundness and Completeness

The Final Algebra

Final algebra semantics are characterised by the opposite assumption to that of initial semantics, namely, that terms must be proved to be distinguishable, otherwise they will be taken to be equivalent. The final algebra (if it exists - see later) is also a model of the theory, that is, all the equations must be satisfied; the difference is that instead of using the equations to show the equivalence of otherwise distinct terms, we use them to prove the distinctness of terms which will otherwise be assumed to be equivalent. In order to do this usefully we must assume the distinctness of certain objects; if we do not assume, for instance, that the constants T and F in Bool are distinguishable in Numbers, then we can construct the degenerate algebra where all the constructors of both sorts are mapped onto the single element of the set tex2html_wrap_inline812 (or the member of any other single-element set). This will (trivially) satisfy all the equations and so be a model; in fact, it is a final model.




Jean Baillie
Thu May 23 16:30:42 BST 1996