New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic. (English) Zbl 0763.03031
Summary: This paper introduces a new higher-order typed constructive predicate logic for fixpoint computations, which exploits the categorical semantics of computations introduced by E. Moggi [Proc. 4th Annual Symp. Logic in Computer Science, 14-23 (1989; Zbl 0716.03007)] and contains a version of P. Martin-Löf’s “iteration type” [“Notes on the domain theoretic interpretation of type theory”, Proc. Workshop Semantics in Programming Languages, Chalmers University (1983)]. The type system enforces a separation of computations from values. The logic contains a novel form of fixpoint induction and can express partial and total correctness statements about evaluation of computations to values. The constructive nature of the logic is witnessed by strong metalogical properties which are proved using a category-theoretic version of the “logical relations” method [G. D. Plotkin, “Denotational semantics with partial functions”, unpublished lecture notes from CSLI Summer School, 1985].
MSC:
| 03F99 | Proof theory and constructive mathematics |
| 03D65 | Higher-type and set recursion theory |
| 68Q55 | Semantics in the theory of computing |
| 03B40 | Combinatory logic and lambda calculus |
| 18D15 | Closed categories (closed monoidal and Cartesian closed categories, etc.) |
| 18C15 | Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads |
Keywords:
monad; higher-order typed constructive predicate logic; fixpoint computations; categorical semantics of computations; fixpoint induction; correctnessCitations:
Zbl 0716.03007References:
| [1] | Coquand, T.; Huet, G., The calculus of constructions, Inform. and Comput., 76, 95 (1988) · Zbl 0654.03045 |
| [2] | Crole, R. L., Programming Metabologics with a Fixpoint Type, (Ph.D. Thesis (1991), University of Cambridge: University of Cambridge U.K) |
| [3] | Crole, R. L.; Pitts, A. A., New foundations for fixpoint computations, (Proceedings, 5th Annual Symposium on Logic In Computer Science (1990), IEEE Computer Society Press: IEEE Computer Society Press Washington), 489-497 · Zbl 0825.68599 |
| [4] | Curien, P.-L., (Categorical Combinators, Sequential Algorithms and Functional Programming (1986), Pitman: Pitman London) · Zbl 0643.68004 |
| [5] | Dummett, M., (Elements of Intuitionism (1977), Oxford Univ. Press) · Zbl 0358.02032 |
| [6] | Freyd, P. J., Algebraically complete categories, (Proceedings, Category Theory 1990. Proceedings, Category Theory 1990, Como. Proceedings, Category Theory 1990. Proceedings, Category Theory 1990, Como, Lecture Notes in Mathematics, Vol. 1488 (1991), Springer-Verlag: Springer-Verlag Berlin), 95-104 · Zbl 0815.18005 |
| [7] | Girard, J.-Y., (Proofs and Types (1989), Cambridge Univ. Press: Cambridge Univ. Press London/New York), (Tr. and with appendices by P. Taylor and Y. Lafont) · Zbl 0671.68002 |
| [8] | Lafont, Y., Logiques, Catégories et Machines, (Ph.D. Thesis (1988), Université de Paris VII) · Zbl 0769.68060 |
| [9] | Lambek, J.; Scott, P. J., Introduction to Higher Order Categorical Logic, (Cambridge Studies in Advanced Mathematics, vol. 7 (1986), Cambridge Univ. Press: Cambridge Univ. Press London/New York) · Zbl 0642.03002 |
| [10] | Lehmann, D. J.; Smyth, M. B., Algebraic specification of data types: A synthetic approach, Math. Systems Theory, 14, 97 (1981) · Zbl 0457.68035 |
| [11] | MacLane, S., (Categories for the Working Mathematician (1971), Springer-Verlag: Springer-Verlag Berlin) · Zbl 0232.18001 |
| [12] | Martin-Löf, P., Notes on the domain theoretic interpretation of type thery, (Proceedings, Workshop on Semantics of Programming Languages. Proceedings, Workshop on Semantics of Programming Languages, Chalmers University (1983)) |
| [13] | Moggi, E., Computational Lambda-Calculus and Monads, (LFCS Technical Report 88-66 (1988), University of Edinburgh) · Zbl 0716.03007 |
| [14] | Moggi, E., Computational lambda-calculus and monads, (Proceedings, 4th Annual Symposium on Logic in Computer Science (1989), IEEE Comput. Soc. Press: IEEE Comput. Soc. Press Washington), 14-23 · Zbl 0716.03007 |
| [15] | Moggi, E., Notions of computations and monads, Inform. and Comput., 93, 55 (1991) · Zbl 0723.68073 |
| [16] | Nordström, B.; Petersson, K.; Smith, J. M., (Programming in Martin-Löf’s Type Theory (1990), Oxford Univ. Press) · Zbl 0744.03029 |
| [17] | Paulson, L. C., (Logic and Computation (1987), Cambridge Univ. Press) · Zbl 0645.68041 |
| [18] | Pitts, A. M., Evaluation logic, (Birtwistle, G., IV Higher Order Workshop. IV Higher Order Workshop, Banff 1990. IV Higher Order Workshop. IV Higher Order Workshop, Banff 1990, Workshops in Computing (1991), Springer-Verlag: Springer-Verlag Berlin), 162-189 |
| [19] | Plotkin, G. D., LCF considered as a programming language, Theoret. Comput. Sci., 5, 223-255 (1977) · Zbl 0369.68006 |
| [20] | Plotkin, G. D., Denotational semantics with partial functions, unpublished lecture notes from CSLI Summer School (1985) |
| [21] | Scott, D. S., A type-theoretic alternative to CUCH, ISWIM, OWHY (1969), University of Oxford, unpublished manuscript · Zbl 0942.68522 |
| [22] | Seely, R. A.G., Hyperdoctrines, natural deduction and the Beck condition, Z. Math. Logik Grundlagen Math., 29, 505 (1983) · Zbl 0565.03032 |
| [23] | Smyth, M. B.; Plotkin, G. D., The category-theoretic solution of recursive domain equations, SIAM J. Comput., 11, 761 (1982) · Zbl 0493.68022 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
