Search

This thesis proposes a generalisation of pre-logical predicates to simply typed formal systems and their categorical models. We analyse the three elements involved in pre-logical predicates -- syntax, semantics and predicates -- within a categorical framework for typed binding syntax and semantics. We then formulate generalised pre-logical predicates and show two distinguishing properties: a) equivalence with the basic lemma and b) closure of binary pre-logical relations under relational composition. To test the adequacy of this generalisation, we derive pre-logical predicates for various calculi and their categorical models including variations of lambda calculi and non-lambda calculi such as many-sorted algebras as well as first-order logic. We then apply generalised pre-logical predicates to characterising behavioural equivalence. Examples of constructive data refinement of typed formal systems are shown, where behavioural equivalence plays a crucial role in achieving data abstraction.