article

Inductive-data-type systems

Authors:

Frédéric Blanqui,

Jean-Pierre Jouannaud,

Mitsuhiro OkadaAuthors Info & Claims

Theoretical Computer Science, Volume 272, Issue 1-2

Pages 41 - 68

https://doi.org/10.1016/S0304-3975(00)00347-9

Published: 06 February 2002 Publication History

Abstract

In a previous work ("Abstract Data Type Systems", TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed λ-calculus enriched by pattern-matching definitions following a certain format, called the "General Schema", which generalizes the usual recursor definitions for natural numbers and similar "basic inductive types". This combined language was shown to be strongly normalizing. The purpose of this paper is to reformulate and extend the General Schema in order to make it easily extensible, to capture a more general class of inductive types, called "strictly positive", and to ease the strong normalization proof of the resulting system. This result provides a computation model for the combination of an algebraic specification language based on abstract data types and of a strongly typed functional language with strictly positive inductive types. Copyright 2002 Elsevier Science B.V.

References

[1]

F. Barbanera, M. Fernndez, Combining first and higher order rewrite systems with type assignment systems, Proc. 1St Internat. ConE on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, vol. 664, Springer, Berlin, 1993.]]

[2]

F. Bathanera, M. Fernndez, Modularity of termination and confluence in combinations of rewrite systems with A, Proc. 20th Internat. Colloq. on Automata, Languages, and Programming, Lecture Notes in Computer Science, vol. 700, Springer, Berlin, 1993.]]

[3]

F. Barbanera, M. Fernndez, H. Geuvers, Modularity of strong normalization and confluence in the algebraic-A-cube. Proc. 9th Symp. on Logic in Computer Science, IEEE Computer Society, 1994.]]

[4]

H. Barendregt, Lambda calculi with types, in: S. Abramski, D.M, Gabbai, T.S.E. Maiboum (Eds.), Handbook of Logic in Computer Science, vol. 2, Oxford University Press, Oxford, 1992.]]

Digital Library

[5]

F. Blanqui, Termination and confluence of higher-order rewrite systems, Proc. I llh Internat. Conf. on Rewriting Techniques and Applications, 2000. Lecture Notes in Computer Science.]]

[6]

F. Blanqui, J-P. Jouannaud, M. Okada, The calculus of algebraic constructions, Proc. 10th Internat. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 1631, Springer, Berlin, 1999.]]

[7]

A. Bouhoula, 3.-P. Jouannaud, 3. Meseguer, Specification and proof in membership equational logic, Theoret. Comput. Sci. 236 (1999).]]

[8]

V. Breazu-Tannen, Combining algebra and higher-order types, Proc. 3rd Symp. on Logic in Computer Science, IEEE Computer Society, 1988.]]

[9]

V. Breazu-Tannen, J. Gallier, Polymorphic rewriting conserves algebraic strong normalization, Proc. 16th Internat. Colloq. on Automata, Languages, and Programming, Lecture Notes in Computer Science, vol. 372, Springer, Berlin, 1989.]]

[10]

V. Breazu-Tannen, J. Gallier, Polymorphic rewriting conserves algebraic strong normalization, Theoret. Comput. Sci. 830) (1991).]]

[11]

H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, M. Tommasi, Tree automata techniques and applications. Available at http://w'ww.grappa.univ-lille3.frltatal, 1997.]]

[12]

T. Coquand, Pattern matching with dependent types, Proc. 3rd Work, on Types for Proofs and Programs, Chalmers University of Technology, Sweden, 1992.]]

[13]

T. Coquand, G. Huet, Constructions: a higher order proof system for mechanizing mathematics, Proc. 1985 European Conf. on Computer Algebra, Lecture Notes in Computer Science, vol. 203, Springer, Berlin, 1985.]]

[14]

T. Coquand, C. Paulin-Mohring, Inductively defined types, Proc. 1988 Internat. Conf. on Computer Logic, Lecture Notes in Computer Science, vol. 417, Springer. Berlin. 1988.]]

[15]

N. de Bruijn, The mathematical language Automath, its usage, and some of its extensions, Proc. Symp. on Automatic Demonstration, Lecture Notes in Computer Science, vol. 125, Springer, Berlin, 1970, (Reprinted in: Selected Papers on Amaranth, in: R.P. Nederpeli, J.H. Geuvers, R,C. de Vrijer (Eds.), Studies in Logic, vol. 133. North-Holland, Amsterdam, 1994).]]

[16]

N. Dershowitz, J.-P. iouannaud, Rewrite systems, in: 3. van Leeuwen (Ed,), Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, chapter 6: Rewrite Systems. North-Holland, Amsterdam, 1990.]]

[17]

0. Dowek, T. Hardin, C. Kirchner. Theorem proving modulo, Tech. Report 3400, INRIA, France, 1998.]]

[18]

0. Dowek, B. Werner, Proof normalization modulo, Tech. Report 3542, INRIA, France, 1998.]]

[19]

J. Gallier, On Girard's "Candidats de Rductibilit", in: P.-G. Odifreddi (Ed.), Logic and Computer Science, North-Holland, Amsterdam, 1990.]]

[20]

E. Gimnez, Codifying guarded definitions with recursion schemes, Proc. 5th Work, on Types for Proofs and Programs, Lecture Notes in Computer Science, vol. 996, Springer, Berlin, 1994.]]

[21]

E. Gimnez, Structural recursive definitions in type theory, Proc. 25th Internet. CoIloq. on Automata, Languages, and Programming, Lecture Notes in Computer Science, vol. 1443, Springer, Berlin, 1998,]]

[22]

J.-Y. Girard, Une extension de linterprtation de Godel a l'analyse, et son application a 'elimination des coupures dans l'analyse et la thorie des types, in: I.E. Feasted (Ed.), Proc. 2nd Scandinavian Logic Symp., of Studies in Logic and the Foundations of Mathematics, vol. 63, North-Holland, Amsterdam, 1971.]]

[23]

J.-Y. Girard, Interpretation fonctionelle et elimination des coupures dans l'arithmetique d'ordre supirieur. Ph.D. Thesis, Universit Paris VII, France, 1972.]]

[24]

J.-Y. Girard, Y. Lafont, P. Taylor, Proofs and Types, Cambridge University Press, Cambridge, 1988.]]

[25]

K. Gddel, On intuitionistic arithmetic and number theory, in: M. Davis (Ed.), The Undecidable, Raven Press, New York, 1965.]]

[26]

K. Hasebe, On extensions of Godel's System T. Master's Thesis, Keio University, Japan, 2000 (in Japanese).]]

[27]

3.-P. Jouannaud, M. Okada, Executable higher-order algebraic specification languages, Proc. 6th Syinp. on Logic in Computer Science, IEEE Computer Society, 1991.]]

[28]

3.-P. .Jouannaud, M. Okada, Abstract data type systems, Theoret. Comput. Sci. 173(2) (1997).]]

Digital Library

[29]

3.-P. Jouannaud, A. Rubio. The higher-order recursive path ordering, Proc. 14th Symp. on Logic in Computer Science, IEEE Computer Society, 1999.]]

Digital Library

[30]

3W. KIop, Combinatory reduction systems, Ph.D. Thesis, University of Utrecht, Netherlands, 1980. Published as Mathematical Center Tract 129.]]

[31]

3W. KIop, V. van Oostrom, F. van Raamsdonk, Combinatory reduction systems: introduction and survey, Theoret. Comput. Sci. 121(1-2) (1993).]]

[32]

P. Martin-L617, An intuitionistic theory of types: predicative part, in: HE. Rose, iC. Shepherdson (Eds.), Proc. 73' Logic CoIIoq., Studies in Logic and the Foundations of Mathematics, vol. 80, North-Holland, Amsterdam, 1975.]]

[33]

P. Martin-Lf, Intuitionistic Type Theory, Bibliopolis, Napels, 1984.]]

[34]

{34 R. Mayr, T. Nipkow, Higher-order rewrite systems and their confluence, Theoret. Comput. Sci. 192 (1998).]]

[35]

N.P. Mendler, First- and second-order lambda calculi with recursive types, Tech. Report TR 86-764, Cornell University, United States, 1986.]]

[36]

NP. Mendler, Inductive definition in type theory, Ph.D. Thesis, Colell University, United States, 1987.]]

[37]

D. Miller, A logic programming language with lambda-abstraction, function variables, and simple unification, Proc. 1989 Internat. Work, on Extensions of Logic Programming, Lecture Notes in Computer Science, vol. 475, Springer, Berlin, 1989.]]

[38]

B. Morale, Automates de formes normales et rductibilit inductive, Master's Thesis, Universit Paris-Sud, France, 1997.]]

[39]

T. Nipkow, Higher-order critical pairs, Proc. 6th Symp. on Logic in Computer Science, IEEE Computer Society, 1991.]]

[40]

M. Okada, in: Strong nonnalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system, Proc. 1989 Internat. Symp. on Symbolic and Algebraic Computation. ACM Press, New York, 1989.]]

[41]

M. Okada, P.3. Scott, A note on rewriting theory for uniqueness of iteration, Theory AppI. Categories, 6(4) (2000).]]

[42]

C. Prehofer, Solving higher-order equations: from logic to programming. Ph.D. Thesis, Technische Universitt MUnchen, Germany, 1995.]]

[43]

Z. Qian, Linear unification of higher-order patterns, Proc. 7th Intermit. Joint Conf, CAAP/FASE on Theory and Practice of Software Development, Lecture Notes in Computer Science, vol. 668, Spnnger, Berlin, 1993.]]

[44]

M.P.A. Sellink, Verifying process algebra proofs in type theory, Proc. Internat. Work, on Semantics of Specification Languages, Workshops in Computing, 1993.]]

[45]

S. Stenlund, Combinators, Lambda-Terms and Proof Theory, D. Reidel, Dordrecht, 1972.]]

[46]

W.W. Tait, Tntensional interpretations of ftinctionals of finite type I, 3. Symbolic Logic 32(2) (1967).]]

[47]

Y. Toyama, Counterexamples to terminating for the direct sum of term rewriting systems, Inform. Process. Len. 25(3) (1986).]]

[48]

J. van de Pol, Termination proofs for higher-order rewrite systems, Proc. 1st Internat. Work, on Higher-Order Algebra, Logic and Term Rewriting, Lecture Notes in Computer Science, vol. 816, Springer, Berlin, 1993.]]

[49]

V. van Oostrom, Confluence for abstract and higher-order rewriting, Ph.D. Thesis, Vrije Universiteit, Netherlands, 1994.]]

[50]

F. van Raamsdonk, Confluence and normalization for higher-order rewriting, Ph.D. Thesis, Vrije Universiteit, Netherlands, 1996.]]

[51]

B. Werner, tine Theme des Constructions Inductives, Ph.D. Thesis, Universit Pans VII, France, 1994.]]

Cited By

Okada MTakahashi Y(2020)A Simplified Application of Howard’s Vector Notation System to Termination Proofs for Typed Lambda-Calculus SystemsRewriting Logic and Its Applications10.1007/978-3-030-63595-4_8(136-155)Online publication date: 25-Apr-2020
https://dl.acm.org/doi/10.1007/978-3-030-63595-4_8
Blanqui F(2016)Termination of rewrite relations on λ-terms based on Girard's notion of reducibilityTheoretical Computer Science10.1016/j.tcs.2015.07.045611:C(50-86)Online publication date: 18-Jan-2016
https://dl.acm.org/doi/10.1016/j.tcs.2015.07.045
Jouannaud JRubio A(2015)Normal Higher-Order TerminationACM Transactions on Computational Logic10.1145/269991316:2(1-38)Online publication date: 9-Mar-2015
https://dl.acm.org/doi/10.1145/2699913
Show More Cited By

Index Terms

Inductive-data-type systems

Recommendations

Type Theory based on Dependent Inductive and Coinductive Types
LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

We develop a dependent type theory that is based purely on inductive and coinductive types, and the corresponding recursion and corecursion principles. This results in a type theory with a small set of rules, while still being fairly expressive. For ...
Mendler-style inductive types, categorically

We present a basis for a category-theoretic account of Mendler-style inductive types. The account is based on suitably defined concepts of Mendler-style algebra and algebra homomorphism; Mendler-style inductive types are identified with initial Mendler-...
Impredicative Encodings of (Higher) Inductive Types
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and consequently do not admit dependent eliminators. To recover η and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Theoretical Computer Science

Theoretical Computer Science Volume 272, Issue 1-2

Special issue on theories of types and proofs

February 6, 2002

391 pages

ISSN:0304-3975

Issue’s Table of Contents

Publisher

Elsevier Science Publishers Ltd.

United Kingdom

Publication History

Published: 06 February 2002

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

29
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Okada MTakahashi Y(2020)A Simplified Application of Howard’s Vector Notation System to Termination Proofs for Typed Lambda-Calculus SystemsRewriting Logic and Its Applications10.1007/978-3-030-63595-4_8(136-155)Online publication date: 25-Apr-2020
https://dl.acm.org/doi/10.1007/978-3-030-63595-4_8
Blanqui F(2016)Termination of rewrite relations on λ-terms based on Girard's notion of reducibilityTheoretical Computer Science10.1016/j.tcs.2015.07.045611:C(50-86)Online publication date: 18-Jan-2016
https://dl.acm.org/doi/10.1016/j.tcs.2015.07.045
Jouannaud JRubio A(2015)Normal Higher-Order TerminationACM Transactions on Computational Logic10.1145/269991316:2(1-38)Online publication date: 9-Mar-2015
https://dl.acm.org/doi/10.1145/2699913
Czajka Ł(2013)Partiality and recursion in higher-order logicProceedings of the 16th international conference on Foundations of Software Science and Computation Structures10.1007/978-3-642-37075-5_12(177-192)Online publication date: 16-Mar-2013
https://dl.acm.org/doi/10.1007/978-3-642-37075-5_12
Hamana M(2009)Semantic labelling for proving termination of combinatory reduction systemsProceedings of the 18th international conference on Functional and Constraint Logic Programming10.1007/978-3-642-11999-6_5(62-78)Online publication date: 28-Jun-2009
https://dl.acm.org/doi/10.1007/978-3-642-11999-6_5
Bertolissi CFernández MAntoy SAlbert E(2008)A rewriting framework for the composition of access control policiesProceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming10.1145/1389449.1389476(217-225)Online publication date: 15-Jul-2008
https://dl.acm.org/doi/10.1145/1389449.1389476
Wack BHoutmann C(2008)Strong normalisation in two pure pattern type systemsMathematical Structures in Computer Science10.1017/S096012950800674918:3(431-465)Online publication date: 1-Jun-2008
https://dl.acm.org/doi/10.1017/S0960129508006749
Blanqui FJouannaud JRubio A(2008)The Computability Path OrderingProceedings of the 22nd international workshop on Computer Science Logic10.1007/978-3-540-87531-4_1(1-14)Online publication date: 16-Sep-2008
https://dl.acm.org/doi/10.1007/978-3-540-87531-4_1
Riba C(2008)Union of Reducibility Candidates for Orthogonal Constructor RewritingProceedings of the 4th conference on Computability in Europe: Logic and Theory of Algorithms10.1007/978-3-540-69407-6_54(498-510)Online publication date: 15-Jun-2008
https://dl.acm.org/doi/10.1007/978-3-540-69407-6_54
Brauner PHoutmann CKirchner C(2007)Superdeduction at workRewriting Computation and Proof10.5555/2391276.2391285(132-166)Online publication date: 1-Jan-2007
https://dl.acm.org/doi/10.5555/2391276.2391285
Show More Cited By

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents