Return to search

A generalisation of pre-logical predicates and its applications

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.

Identiferoai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:561900
Date January 2005
CreatorsKatsumata, Shin-ya
ContributorsSannella, Donald. : Stark, Ian
PublisherUniversity of Edinburgh
Source SetsEthos UK
Detected LanguageEnglish
TypeElectronic Thesis or Dissertation
Sourcehttp://hdl.handle.net/1842/850

Page generated in 0.0016 seconds