Abstract
We investigate (co-)induction in Classical Logic under the propositions-as-types paradigm, considering propositional, second-order, and (co-)inductive types. Specifically, we introduce an extension of the Dual Calculus with a Mendler-style (co-)iterator that remains strongly normalizing under head reduction. We prove this using a non-constructive realizability argument.
M.D. Campos—This work was supported by the United Kingdom’s Engineering and Physical Sciences Research Council [grant number EP/J500380/1].
M. Fiore—Partially supported by ERC ECSYM.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Unlike Wadler’s presentation, we keep the standard practice of avoiding suffix operators; whilst lexical duality is lost, we think it improves readability.
- 2.
- 3.
A non-terminating, non-well-typed cut: \(\alpha .\left( not\left\langle \alpha \right\rangle \mathbin {\bullet }\alpha \right) \mathbin {\bullet }not\left[ \alpha .\left( not\left\langle \alpha \right\rangle \mathbin {\bullet }\alpha \right) \right] \).
- 4.
We note that the original presentation of this inductive operator [15] was in System F and, accordingly, the operator considered instead functionals of type \({\forall X . (X \rightarrow A) \rightarrow F(X) \rightarrow A}\). Cognoscenti will recognize that this type is the type-theoretic Yoneda reformulation \({\forall X . (X \rightarrow A) \rightarrow T(X)}\) of \(T(A)=F(A)\rightarrow A\) for \(T(X)=F(X)\rightarrow A\).
- 5.
One may wonder if the output continuation is strictly necessary. As outputs appear on the right of sequents, and the induction is already a left-rule, the only possible alternative would be to add a co-variable to represent it. However, under this rule the system would no longer be closed under substitution [13].
- 6.
Cognoscenti will recognize that they are point-wise Kan extensions.
References
Abel, A., Matthes, R., Uustalu, T.: Iteration and coiteration schemes for higher-order and nested datatypes. Theor. Comput. Sci. 333(1), 3–66 (2005)
Ahn, K.Y., Sheard, T.: A hierarchy of Mendler style recursion combinators: Taming inductive datatypes with negative occurrences. In: Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, pp. 234–246. ACM, New York (2011)
Barbanera, F., Berardi, S.: A symmetric lambda calculus for classical program extraction. Inf. Comput. 125(2), 103–117 (1996)
Barbanera, F., Berardi, S., Schivalocchi, M.: “Classical” programming-with-proofs in \(\lambda ^{Sym}_{PA}\) : An analysis of non-confluence. In: Abadi, M., Ito, T. (eds.) Theoretical Aspects of Computer Software. Lecture Notes in Computer Science, vol. 1281, pp. 365–390. Springer, Berlin Heidelberg (1997)
Crolard, T.: A formulae-as-types interpretation of subtractive logic. J. Log. Comput. 14(4), 529–570 (2004)
Curien, P.L., Herbelin, H.: The duality of computation. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming ICFP 2000, pp. 233–243. ACM, New York (2000)
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (2002)
Dawar, A., Gurevich, Y.: Fixed point logics. Bull. Symb. Log. 8(01), 65–88 (2002)
Dougherty, D.J., Ghilezan, S., Lescanne, P., Likavec, S.: Strong normalization of the dual classical sequent calculus. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 169–183. Springer, Heidelberg (2005)
Gentzen, G.: Investigations into logical deduction. Am. Philos. Q. 1(4), 288–306 (1964)
Harper, B., Lillibridge, M.: ML with callcc is unsound. Post to TYPES mailing list (1991)
Hur, C.K., Neis, G., Dreyer, D., Vafeiadis, V.: The power of parameterization in coinductive proof. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2013, pp. 193–206. ACM, New York (2013)
Kimura, D., Tatsuta, M.: Dual Calculus with inductive and coinductive types. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 224–238. Springer, Heidelberg (2009)
Matthes, R.: Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. Ph.D. thesis, Ludwig-Maximilians Universität, May 1998
Mendler, N.: Inductive types and type constraints in the second-order lambda calculus. Ann. Pure Appl. Log. 51(1), 159–172 (1991)
Parigot, M.: Strong normalization of second order symmetric \(\lambda \)-calculus. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol. 1974, pp. 442–453. Springer, Heidelberg (2000)
Tzevelekos, N.: Investigations on the Dual Calculus. Theor. Comput. Sci. 360(1), 289–326 (2006)
Uustalu, T., Vene, V.: Mendler-style inductive types, categorically. Nord. J. Comput. 6(3), 343 (1999)
Wadler, P.: Call-by-value is dual to call-by-name. In: Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming ICFP 2003, pp. 189–201. ACM, New York (2003)
Acknowledgments
Thanks to Anuj Dawar, Tim Griffin, Ohad Kammar, Andy Pitts, and the anonymous referees for their comments and suggestions.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Devesas Campos, M., Fiore, M. (2016). Classical Logic with Mendler Induction. In: Artemov, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2016. Lecture Notes in Computer Science(), vol 9537. Springer, Cham. https://doi.org/10.1007/978-3-319-27683-0_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-27683-0_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-27682-3
Online ISBN: 978-3-319-27683-0
eBook Packages: Computer ScienceComputer Science (R0)