Manfred Schmidt-Schauß
David Sabel
ABSTRACT
This paper presents an algorithm for unification of meta-expressions of higher-order lambda calculi with recursive bindings. The meta-language uses higher-order abstract syntax. Besides usual unification variables for expressions and term variables, there are context-variables for generalized shapes of contexts, environment variables for sets of bindings, and (flexible) chain-variables as they, for instance, occur in formal descriptions of the operational semantics of lazy functional programming languages with shared environments. To exclude solutions with unintended scoping, the algorithm takes advantage of so-called non-capture constraints. The expressiveness of the meta-language comprises reduction contexts to support reasoning on program evaluation under reduction strategies. The non-deterministic unification algorithm runs in polynomial time provided certain restrictions on the number of occurrences of unification variables hold. The deterministic version of the algorithm will output a finite and concise set of representatives of all solutions. Results on an implementation of the algorithm are presented. The experiments focus on computing critical pairs of equations from program calculi modeling lazy functional languages which support the reasoning on the correctness of program transformations.
- Z. M. Ariola and M. Felleisen. The call-by-need lambda calculus. J. Funct. Program., 7(3):265--301, 1997. Google Scholar
Digital Library
- Z. M. Ariola, M. Felleisen, J. Maraist, M. Odersky, and P. Wadler. A call-by-need lambda calculus. In POPL 1995, pp. 233--246. ACM, 1995. Google ScholarDigital Library
- F. Baader and W. Snyder. Unification theory. In J. A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pp. 445--532. Elsevier and MIT Press, 2001.Google Scholar
- J. Cheney. Toward a general theory of names: Binding and scope. In MERLIN 2005, pp. 33--40. ACM, 2005. Google ScholarDigital Library
- G. P. Huet. A unification algorithm for typed lambda-calculus. Theor. Comput. Sci., 1(1):27--57, 1975.Google ScholarCross Ref
- A. Jez. Context unification is in PSPACE. In ICALP 2014, LNCS 8573, pp. 244--255. Springer, 2014.Google Scholar
- E. Machkasova and F. A. Turbak. A calculus for link-time compilation. In ESOP 2000, LNCS 1782, pp. 260--274. Springer, 2000. Google ScholarDigital Library
- A. K. D. Moran, D. Sands, and M. Carlsson. Erratic fudgets: A semantic theory for an embedded coordination language. Sci. Comput. Program., 46(1-2):99--135, 2003. Google ScholarDigital Library
- F. Pfenning and C. Elliott. Higher-order abstract syntax. In PLDI 1988, pp. 199--208. ACM, 1988. Google ScholarDigital Library
- C. Rau, D. Sabel, and M. Schmidt-Schauß. Correctness of program transformations as a termination problem. In IJCAR 2012, LNCS 7364, pp. 462--476. Springer, 2012. Google ScholarDigital Library
- C. Rau and M. Schmidt-Schauß. A unification algorithm to compute overlaps in a call-by-need lambda-calculus with variable-binding chains. In UNIF 2011, pp. 35--41, July 2011.Google Scholar
- D. Sabel and M. Schmidt-Schauß. A call-by-need lambda-calculus with locally bottom-avoiding choice: Context lemma and correctness of transformations. Math. Structures Comput. Sci., 18(03):501--553, 2008. Google ScholarDigital Library
- T. J. Schaefer. The complexity of satisfiability problems. In STOC 1978, pp. 216--226. ACM, 1978. Google ScholarDigital Library
- M. Schmidt-Schauß. Decidable variants of higher-order unification. In Mechanizing Mathematical Reasoning, Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday, LNCS 2605, pp. 154--168. Springer, 2005.Google Scholar
- M. Schmidt-Schauß, T. Kutsia, J. Levy, and M. Villaret. Nominal unification of higher order expressions with recursive let, 2016. submitted to a conference.Google Scholar
- M. Schmidt-Schauß, C. Rau, and D. Sabel. Algorithms for Extended Alpha-Equivalence and Complexity. In RTA 2013, LIPIcs 21, pp. 255--270. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, 2013.Google Scholar
- M. Schmidt-Schauß and D. Sabel. Improvements in a functional core language with call-by-need operational semantics. In PPDP 2015, pp. 220--231. ACM, 2015. Google ScholarDigital Library
- M. Schmidt-Schauß, D. Sabel, and E. Machkasova. Simulation in the call-by-need lambda-calculus with letrec. In RTA 2010, LIPIcs 6, pp. 295--310. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010.Google Scholar
- M. Schmidt-Schauß, D. Sabel, and E. Machkasova. Simulation in the call-by-need lambda-calculus with letrec, case, constructors, and seq. Log. Methods Comput. Sci., 11(1), 2015.Google Scholar
- M. Schmidt-Schauß, M. Schütz, and D. Sabel. Safety of Nöcker's strictness analysis. J. Funct. Programming, 18(04):503--551, 2008. Google ScholarDigital Library
- P. Sestoft. Deriving a lazy abstract machine. J. Funct. Programming, 7(3):231--264, 1997. Google ScholarDigital Library
- C. Urban and C. Kaliszyk. General bindings and alpha-equivalence in nominal isabelle. Log. Methods Comput. Sci., 8(2), 2012.Google Scholar
- C. Urban, A. M. Pitts, and M. Gabbay. Nominal unification. In CSL 2003, LNCS 2803, pp. 513--527. Springer, 2003.Google ScholarCross Ref
- J. B. Wells, D. Plump, and F. Kamareddine. Diagrams for meaning preservation. In RTA 2003, LNCS 2706, pp. 88--106. Springer, 2003. Google ScholarDigital Library
Index Terms
- Unification of program expressions with recursive bindings
Recommendations
Decidability of bounded second order unification
It is well-known that first order unification is decidable, whereas second order (and higher order) unification is undecidable. Bounded second order unification is second order unification under the restriction that only a bounded number of bound ...
Undecidability of the unification and admissibility problems for modal and description logics
We show that the unification problem “is there a substitution instance of a given formula that is provable in a given logic?” is undecidable for basic modal logics K and K4 extended with the universal modality. It follows that the admissibility problem ...
Derivation and inference of higher-order strictness types
We extend an existing first-order typing system for strictness analysis to the fully higher-order case, covering both the derivation system and the inference algorithm. The resulting strictness typing system has expressive capabilities far beyond that ...
Comments