Deriving Logical Relations from Interpretations of Predicate Logic
| Autor: | Claudio Hermida, Edmund Robinson, Uday S. Reddy |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Predicate logic
Interpretation (logic) General Computer Science Computer science 020207 software engineering 0102 computer and information sciences 02 engineering and technology Pullback (category theory) Extension (predicate logic) Type (model theory) Monad (functional programming) Adjunction 01 natural sciences Predicate (grammar) Theoretical Computer Science Logical relations Algebra TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Mathematics::Category Theory Computer Science::Logic in Computer Science 0202 electrical engineering electronic engineering information engineering Computer Science::Programming Languages |
| Zdroj: | MFPS |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/j.entcs.2019.09.013 |
| Popis: | This paper extends the results of Hermida's thesis about logical predicates to more general logical relations and a wider collection of types. The extension of type constructors from types to logical relations is derived from an interpretation of those constructors on a model of predicate logic. This is then further extended to n-ary relations by pullback. Hermida's theory shows how right adjoints in the category of fibrations are composed from a combination of Cartesian lifting and a local adjunction. This result is generalised to make it more applicable to left adjoints, and then shown to be stable under pullback, deriving an account of n-ary relations from standard predicate logic. A brief discussion of lifting monads to predicates includes the existence of an initial such lifting, generalising existing results. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect