×

zbMATH — the first resource for mathematics

Unification for \(\lambda\)-calculi without propagation rules. (English) Zbl 06667707
Sampaio, Augusto (ed.) et al., Theoretical aspects of computing – ICTAC 2016. 13th international colloquium, Taipei, Taiwan, ROC, October 24–31, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-46749-8/pbk; 978-3-319-46750-4/ebook). Lecture Notes in Computer Science 9965, 179-195 (2016).
Summary: We present a unification procedure for calculi with explicit substitutions (ES) without propagation rules. The novelty of this work is that the unification procedure was developed for the calculi with ES that belong to the paradigm known as “act at a distance”, i.e. explicit substitutions are not propagated to the level of variables, as usual. The unification procedure is proved correct and complete, and enjoy a simple form of substitution, called grafting, instead of the standard capture avoiding variable substitution.
For the entire collection see [Zbl 1347.68012].
MSC:
68Qxx Theory of computing
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit substitutions. J. Funct. Program. 1(4), 375–416 (1991) · Zbl 0941.68542 · doi:10.1017/S0956796800000186
[2] Accattoli, B.: An abstract factorization theorem for explicit substitutions. In: Tiwari [36], pp. 6–21
[3] Accattoli, B., Barenbaum, P., Mazza, D.: Distilling abstract machines. In: Jeuring, J., Chakravarty, M.M.T. (eds.) Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, Gothenburg, Sweden, 1–3 September 2014, pp. 363–376. ACM (2014) · Zbl 1345.68036 · doi:10.1145/2692915.2628154
[4] Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C.: A nonstandard standardization theorem. In: Jagannathan, S., Sewell, P. (eds.) POPL, pp. 659–670. ACM (2014) · Zbl 1284.68121 · doi:10.1145/2535838.2535886
[5] Accattoli, B., Kesner, D.: The structural \[ \lambda \] -calculus. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 381–395. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-15205-4_30 · Zbl 1287.03034 · doi:10.1007/978-3-642-15205-4_30
[6] Accattoli, B., Kesner, D.: The permutative \[ \lambda \] -calculus. In: Bjørner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 23–36. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-28717-6_5 · Zbl 1352.03019 · doi:10.1007/978-3-642-28717-6_5
[7] Accattoli, B., Kesner, D.: Preservation of strong normalisation modulo permutations for the structural lambda-calculus. Logical Methods Comput. Sci. 8(1), 1–44 (2012) · Zbl 1237.03011 · doi:10.2168/LMCS-8(1:28)2012
[8] Accattoli, B., Dal Lago, U.: On the invariance of the unitary cost model for head reduction. In: Tiwari [36], pp. 22–37
[9] Ayala-Rincón, M., Kamareddine, F.: Unification via the \[ \lambda s_e \] -style of explicit substitution. Logical J. IGPL 9(4), 489–523 (2001) · Zbl 0987.03012 · doi:10.1093/jigpal/9.4.489
[10] Ayala-Rincón, M., Kamareddine, F.: On applying the \[ \lambda s_e \] -style of unification for simply-typed higher order unification in the pure lambda calculus. Matemática Contemporânea 24, 1–22 (2003) · Zbl 1073.03007
[11] de Moura, F.L.C., Kesner, D., Ayala-Rincón, M.: Metaconfluence of calculi with explicit substitutions at a distance. In: Raman, V., Suresh, S.P. (eds.) 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), vol. 29, pp. 391–402. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2014) · Zbl 1360.68324
[12] de Moura, F.L.C.: Higher-order unification via explicit substitutions at a distance. In: LSFA 2014 (2014). Accepted for short presentation
[13] de Moura, F.L.C., Ayala-Rincón, M., Kamareddine, F.: Higher-order unification: a structural relation between Huet’s method and the one based on explicit substitutions. J. Appl. Logic 6(1), 72–108 (2008) · Zbl 1138.03014 · doi:10.1016/j.jal.2006.10.001
[14] de Moura, F.L.C., Kamareddine, F., Ayala-Rincón, M.: Second-order matching via explicit substitutions. In: Baader, F., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3452, pp. 433–448. Springer, Heidelberg (2005). doi: 10.1007/978-3-540-32275-7_29 · Zbl 1108.03308 · doi:10.1007/978-3-540-32275-7_29
[15] Dougherty, D.J.: Higher-order unification via combinators. TCS 114(2), 273–298 (1993) · Zbl 0772.68061 · doi:10.1016/0304-3975(93)90075-5
[16] Dowek, G.: Third order matching is decidable. APAL 69, 135–155 (1994) · Zbl 0822.03010
[17] Dowek, G.: Higher-order unification and matching. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, pp. 1009–1062. MIT press and Elsevier (2001). Chap. 16 · Zbl 1011.03005 · doi:10.1016/B978-044450813-3/50018-7
[18] Dowek, G., Hardin, T., Kirchner, C.: Higher order unification via explicit substitutions. Inf. Comput. 157(1–2), 183–235 (2000) · Zbl 1005.03016 · doi:10.1006/inco.1999.2837
[19] Briaud, D., Lescanne, P., Rouyer-Degli, J.: \[ \lambda \upsilon \] , a calculus of explicit substitutions which preserves strong normalization. JFP 6(5), 699–722 (1996) · Zbl 0873.68108
[20] Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987) · Zbl 0625.03037 · doi:10.1016/0304-3975(87)90045-4
[21] Goldfarb, W.: The undecidability of the second-order unification problem. Theoret. Comput. Sci. 13(2), 225–230 (1981) · Zbl 0457.03006 · doi:10.1016/0304-3975(81)90040-2
[22] Guillaume, B.: The \[ \lambda s_e \] -calculus does not preserve strong normalization. J. Func. Program. 10(4), 321–325 (2000) · Zbl 0971.68021 · doi:10.1017/S0956796800003695
[23] Huet, G.: The undecidability of unification in third order logic. Inf. Control 22(3), 257–267 (1973) · Zbl 0257.02038 · doi:10.1016/S0019-9958(73)90301-X
[24] Huet, G.: A unification algorithm for typed lambda-calculus. TCS 1(1), 27–57 (1975) · Zbl 0332.02035 · doi:10.1016/0304-3975(75)90011-0
[25] Huet, G.: Résolution d’équations dans les langages d’ordre 1,2,.., \[ \omega \] . Ph.D. thesis, University Paris-7 (1976)
[26] Kamareddine, F., Ríos, A.: Extending a \[ \lambda \] -calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms. J. Func. Program. 7, 395–420 (1997) · Zbl 0882.03011 · doi:10.1017/S0956796897002785
[27] Kesner, D.: A theory of explicit substitutions with safe and full composition. Logical Methods Comput. Sci. 5(31), 1–29 (2009) · Zbl 1168.68008
[28] Lins, R.D.: A new formula for the execution of categorical combinators. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 89–98. Springer, Heidelberg (1986). doi: 10.1007/3-540-16780-3_82 · Zbl 0642.68030 · doi:10.1007/3-540-16780-3_82
[29] Loader, R.: Higher order \[ \beta \] matching is undecidable. Logic J. Interest Group Pure Appl. Logics 11(1), 51–68 (2003) · Zbl 1014.03017
[30] Mellies, P.-A.: Typed \[ \lambda \] -calculi with explicit substitutions may not terminate. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 328–334. Springer, Heidelberg (1995). doi: 10.1007/BFb0014062 · Zbl 1063.03522 · doi:10.1007/BFb0014062
[31] Milner, R.: Local bigraphs and confluence: two conjectures: (extended abstract). ENTCS 175(3), 65–73 (2007) · Zbl 1277.68197
[32] Padovani, V.: Decidability of fourth-order matching. Math. Struct. Comput. Sci. 10(3), 361–372 (2000) · Zbl 0954.03017 · doi:10.1017/S0960129500003108
[33] Renaud, F.: Metaconfluence of \[ {\lambda }\mathtt{j} \] : dealing with non-deterministic replacements (2011). http://www.pps.univ-paris-diderot.fr/ renaud/lambdaj_mconf.pdf
[34] Snyder, W., Gallier, J.H.: Higher-order unification revisited: complete sets of transformations. J. Symb. Comput. 8(1/2), 101–140 (1989) · Zbl 0682.03034 · doi:10.1016/S0747-7171(89)80023-9
[35] Stirling, C.: A game-theoretic approach to deciding higher-order matching. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 348–359. Springer, Heidelberg (2006). doi: 10.1007/11787006_30 · Zbl 1133.03315 · doi:10.1007/11787006_30
[36] Tiwari, A. (ed.) 23rd International Conference on Rewriting Techniques and Applications (RTA 2012). LIPIcs, Nagoya, Japan, 28 May 2012 – 2 June 2012, vol. 15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)
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.