The approximation theorem for the \(\Lambda_{\mu}\)-calculus. (English) Zbl 1423.03052
Summary: We consider a notion of approximation for terms of de Groote-Saurin \(\Lambda_{\mu}\)-calculus. Then, we introduce an intersection type assignment system for that calculus which is invariant under subject conversion. The type assignment system also induces a filter model, which is an extensional \(\Lambda_{\mu}\)-model in the sense of K. Nakazawa and S. Katsumata [“Extensional models of untyped lambda-mu calculus”, Electron. Proc. Theor. Comput. Sci. (EPTCS) 97, 35–47 (2012; doi:10.4204/EPTCS.97.3]. We then establish the approximation theorem, stating that a type can be assigned to a term in the system if and only if it can be assigned to same of its approximations.
MSC:
| 03B40 | Combinatory logic and lambda calculus |
References:
| [1] | AbramskyS. (1991). Domain theory in logical form. Annals of Pure and Applied Logic51(1-2)1-77.10.1016/0168-0072(91)90065-T · Zbl 0737.03006 · doi:10.1016/0168-0072(91)90065-T |
| [2] | BarendregtH. P. (1984). The Lambda Calculus - Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics volume 103, North-Holland. · Zbl 0551.03007 |
| [3] | BarendregtH. P., CoppoM. and Dezani-CiancagliniM. (1983). A filter lambda model and the completeness of type assignment. Journal Symbolic Logic48(4)931-940.10.2307/2273659 · Zbl 0545.03004 |
| [4] | DavidR. and P.Walter. (2001). λμ-calculus and Böhm’s theorem. Journal Symbolic Logic66(1)407-413.10.2307/2694930 · Zbl 0981.03019 |
| [5] | Dezani-CiancagliniM., HonsellF. and MotohamaY. (2001). Approximation theorems for intersection type systems. Journal of Logicand Computation11(3)395-417.10.1093/logcom/11.3.395 · Zbl 0984.03013 |
| [6] | de GrooteP. (1994a). A CPS-translation of the Lambda-μ-calculus. In: CAAP. Lecture Notes in Computer Science78785-99.10.1007/BFb0017475 · Zbl 0938.03024 |
| [7] | de GrooteP. (1994b). On the relation between the lambda-mu-calculus and the syntactic theory of sequential control. In: LPAR. Springer Lecture Notes in Computer Science 31-43. |
| [8] | HerbelinH. and GhilezanS. (2008). An approach to call-by-name delimited continuations. In: Proceedings of POPL’08 383-394. · Zbl 1295.68063 |
| [9] | NakazawaK. and KatsumataS. (2012). Extensional models of untyped Λ-μ calculus. In: Proceedings of Fourth Workshop on Classical Logic and Computation (CL&C’12). Electronic Proceedings in Theoretical Computer Science, 9735-47.10.4204/EPTCS.97.3 |
| [10] | ParigotM. (1992). An algorithmic interpretation of classical natural deduction. In: Proceedings of 3rd International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR’92). Springer Lecture Notes in Computer Science624190-201.10.1007/BFb0013061 · Zbl 0925.03092 |
| [11] | PyW. (1998). Confluence en λμ-calcul, Ph.D. thesis, Universite de Savoie. |
| [12] | SaurinA. (2005). Separation with streams in the λμ-calculus. In: Proceedings of LICS’05 356-365. |
| [13] | SaurinA. (2008a). Une étude logique du contrôle (appliquée à la programmation fonctionnelle et logique). PhD thesis, École Polytechnique. |
| [14] | SaurinA. (2008b). On the relations between the syntactic theories of λμ-calculi. In: CSL. Lecture Notes in Computer Science5213154-168.10.1007/978-3-540-87531-4_13 · Zbl 1156.03317 |
| [15] | SaurinA. (2010a). Standardization and Böhm trees for λμ calculus. In: Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings. Lecture Notes in Computer Science6009134-149.10.1007/978-3-642-12251-4_11 · Zbl 1284.68137 |
| [16] | SaurinA. (2010b). A Hierarchy for delimited continuations in call-by-name. In: Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings. Lecture Notes in Computer Science6014374-388.10.1007/978-3-642-12032-9_26 · Zbl 1284.03139 |
| [17] | SaurinA. (2010c). Typing streams in the λμ-calculus. ACM Transactions on Computational Logic, 11(4). · Zbl 1351.68065 |
| [18] | SaurinA. (2012). Böhm theorem and Böhm trees for the λμ-calculus. Theoretical Computer Science435106-138.10.1016/j.tcs.2012.02.027 · Zbl 1244.68027 · doi:10.1016/j.tcs.2012.02.027 |
| [19] | StreicherT. and ReusB. (1998). Classical logic, continuation semantics and abstract machines. Journalof Functional Programming, 8(6)543-572.10.1017/S0956796898003141 · Zbl 0928.68074 |
| [20] | van BakelS., BarbaneraF. and de’LiguoroU. (2011). A filter model for λμ. In: LukeO. (ed.) Proceedings of TLCA’11. ARCoSS/Lecture Notes in Computer Science6690213-228.10.1007/978-3-642-21691-6_18 · Zbl 1331.03021 |
| [21] | van BakelS., BarbaneraF. and de’LiguoroU. (2013) Characterisation of strongly normalising λμ-terms. In: Post Proceedings of ITRS’12. Electronic Proceedings in Theoretical Computer Science. To appear. |
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.
