×

Structural induction and coinduction in a fibrational setting. (English) Zbl 0941.18006

A categorical logic formulation of induction and coinduction is proposed. The main results provide criteria for the validity of such principles: in the presence of comprehension, the induction principle for initial algebras is admissible, and in the presence of quotient types, the coinduction principle for terminal coalgebras is admissible. One of the main points is to give formulation, in a canonical fashion, of an induction principle for initial algebras and a coinduction principle for terminal coalgebras using polynomial functors. The results on validity of the induction and coinduction principles (main results of the paper) are presented as admissibility properties of constructive predicate logic. Using this, the authors give a reasoning principle for recursive data types involving mixed variance functors. The connections with contextual and functional completeness, internal full abstraction, adequacy and strong extensionality are considered. It is argued that the level of abstraction achieved in the paper is the right level of abstraction to combine salient features of the above approaches.

MSC:

18B20 Categories of machines, automata
68Q55 Semantics in the theory of computing
03D65 Higher-type and set recursion theory
03G99 Algebraic logic
PDF BibTeX XML Cite
Full Text: DOI Link

References:

[1] Aczel, P.; Mendler, N., A final coalgebra theorem, Category theory and computer science, Springer LNCS 389, (1989), Springer-Verlag Berlin, p. 357-365
[2] Abramsky, S.; Jung, A., Domain theory, (), 1-68
[3] America, P.; Rutten, J., Solving reflexive domain equations in a category of complete metric spaces, J. comp. syst. sci., 39, 343-375, (1989) · Zbl 0717.18002
[4] Arbib, M.A.; Manes, E.G., Arrows, structures and functors. the categorical imperative, (1975), Academic Press New York · Zbl 0374.18001
[5] Arbib, M.A.; Manes, E.G., Parametrized data types do not need highly constrained parameters, Inform. contr., 52, 139-158, (1982) · Zbl 0505.68013
[6] Backhouse, R. Bijsterveld, M. 1994, The “Beautiful Theorem” Univ. Eindhoven
[7] de Bakker, J.; Vink, E., Control flow semantics, (1996), The MIT Press Boston · Zbl 0941.68079
[8] Barr, M., Algebraically compact functors, J. pure appl. alg., 82, 211-231, (1992) · Zbl 0777.18005
[9] Cockett, J.R.B., Introduction to distributive categories, Math. struct. comp. science, 1, 1-20, (1991) · Zbl 0715.18005
[10] Cockett, J.R.B.; Spencer, D., Strong categorical datatypes I, (), 141-169 · Zbl 0792.18008
[11] Cockett, J.R.B.; Spencer, D., Strong categorical datatypes II: A term logic for categorical programming, Theor. comp. sci., 139, 69-113, (1995) · Zbl 0874.68033
[12] Crole, R.L., Categories for types, (1993), Cambridge Univ. Press Cambridge · Zbl 0837.68077
[13] Crole, R.L.; Pitts, A.M., New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic, Inform. comput., 98, 171-210, (1992) · Zbl 0763.03031
[14] Ehrhard, Th., A categorical semantics of constructions, Logic in comp. sci. 3, (1988), IEEE Comp. Sci. Press Los Alamitos, p. 264-273
[15] Fiech, A. 1992, Colimits in the category Cpo, Kansas State University · Zbl 0870.18001
[16] Fiore, M., A coinduction principle for recursive data types based on bisimulation, Inform. comput., 127, 186-198, (1996) · Zbl 0868.68054
[17] Fiore, M., Axiomatic domain theory in categories of partial maps, (1996), Cambridge Univ. Press Cambridge · Zbl 0979.68549
[18] Freyd, P.J., Recursive types reduced to inductive types, Logic in comp. sci. 5, (1990), IEEE Comp. Sci. Press Los Alamitos, p. 498-507
[19] Freyd, P.J., Remarks on algebraically compact categories, (), 95-106 · Zbl 0803.18002
[20] Freyd, P.J.; Scedrov, A., Categories, allegories, Math. library 39, (1990), North-Holland Amsterdam
[21] Goguen, J.A.; Thatcher, J.; Wagner, E., An initial algebra approach to the specification, correctness and implementatiton of abstract data types, (), 80-149
[22] Hagino, T., A typed lambda calculus with categorical type constructors, (), 140-157
[23] Hensel, U.; Jacobs, B., Proof principles for datatypes with iterated recursion, (), 220-241 · Zbl 0887.68069
[24] Hermida, C., Fibrations, logical predicates and indeterminates, Techn. rep., (1993)
[25] Hermida, C. Some properties of Fib as a fibred 2-category, J. Pure Appl. Algebra · Zbl 0935.18007
[26] Hermida, C.; Jacobs, B., An algebraic view of structural induction, (), 412-426 · Zbl 1044.68678
[27] Hermida, C.; Jacobs, B., Fibrations with indeterminates: contextual and functional completeness for polymorphic lambda calculi, Math. struct. comp. sci., 5, 501-531, (1995) · Zbl 0844.03003
[28] Jacobs, B., Categorical type theory, (1991), Univ. Nijmegen
[29] Jacobs, B., Comprehension categories and the semantics of type dependency, Theor. comp. sci., 107, 169-207, (1993) · Zbl 0804.18007
[30] Jacobs, B., Semantics of weakening and contraction, Ann. pure appl. logic, 69, 73-106, (1994) · Zbl 0814.03007
[31] Jacobs, B. 1994, Quotients in simple type theory, Univ. of Utrecht
[32] Jacobs, B., Parameters and parametrization in specification using distributive categories, Fund. informaticae, 24, 209-250, (1995) · Zbl 0831.68064
[33] Jacobs, B., Invariants, bisimulations and the correctness of coalgebraic refinements, (), 276-291
[34] Joyal, A.; Moerdijk, I., Algebraic set theory, (1995), Cambridge Univ. Press Cambridge · Zbl 0847.03025
[35] Kelly, G.M., Elementary observations on 2-categorical limits, Bull. austr. math. soc., 39, 301-317, (1989) · Zbl 0657.18004
[36] Lambek, J.; Scott, P.J., Introduction to higher-order categorical logic, Studies in adv. math. 7, (1986), Cambridge Univ. Press Cambridge · Zbl 0596.03002
[37] Lawvere, F.W., Equality in hyperdoctrines and comprehension scheme as an adjoint functor, (), 1-14
[38] Lehmann, D.; Smyth, M., Algebraic specification of datatypes: A synthetic approach, Math. systems theory, 14, 97-139, (1981) · Zbl 0457.68035
[39] Makkai, M., The fibrational formulation of intuitionistic predicate logic I: completeness according to Gödel, Kripke, and Läuchli. part 1, Notre dame J. formal logic, 34, 334-377, (1993) · Zbl 0808.03049
[40] Makkai, M., The fibrational formulation of intuitionistic predicate logic I: completeness according to Gödel, Kripke, and Läuchli, Notre dame J. formal logic, 34, 471-499, (1993) · Zbl 0808.03050
[41] Manes, E.G.; Arbib, M.A., Algebraic approaches to program semantics, (1986), Springer/AKM Theor. Comp. Sci Berlin · Zbl 0599.68008
[42] Markowsky, G., Categories of chain-complete posets, Theor. comp. sci., 4, 125-135, (1977) · Zbl 0366.18003
[43] Pavlović, D., Predicates and fibrations, (1990), Univ. Utrecht
[44] Pavlović, D. 1995, Maps I: Relative to a factorization system, J. Pure Appl. Algebra, 60, 1995, 9, 34
[45] Pavlović, D., Maps II: chasing diagrams in categorical proof theory, J. igpl, 4, 1-36, (1996) · Zbl 0852.18008
[46] Pitts, A.M., A co-induction principle for recursively defined domains, Theor. comp. sci., 124, 195-219, (1994) · Zbl 0795.68129
[47] Pitts, A.M., Relational properties of domains, Inform. comput., 127, 66-90, (1996) · Zbl 0868.68037
[48] Plotkin, G.; Abadi, M., A logic for parametric polymorphism, (), 361-375 · Zbl 0788.68091
[49] Reichel, H., An approach to object semantics based on terminal co-algebras, Math. struct. comp. sci., 5, 129-152, (1995) · Zbl 0854.18006
[50] Rutten, J.; Turi, D., On the foundations of final semantics: non-standard sets, metric spaces and partial orders, (), 477-530
[51] Rutten, J.; Turi, D., Initial algebra and final coalgebra semantics for concurrency, (), 530-582
[52] Smyth, M.B., Topology, (), 641-761
[53] Smyth, M.B.; Plotkin, G.D., The category theoretic solution of recursive domain equations, SIAM J. comput., 11, 761-783, (1982) · Zbl 0493.68022
[54] Street, R., The formal theory of monads, J. pure appl. algebra, 2, 149-168, (1972) · Zbl 0241.18003
[55] Street, R., Fibrations and Yoneda’s lemma in a 2-category, (), 104-133
[56] Street, R.; Walters, Yoneda structures on 2-categories, J. algebra, 50, 350-379, (1978) · Zbl 0401.18004
[57] Wirsing, M., Algebraic specification, (), 673-788 · Zbl 0900.68309
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.