Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type

DOI10.1007/3-540-61464-8_64MaRDI QIDQ5055872zbMATH OpenOpenAlexFDO

Authors Roland Fettig, Bernd Löchner

Publication date 9 December 2022

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61464-8_64

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Recommendations

• Linear unification of higher-order patterns
• Higher-order unification via combinators
• Two thoughts on higher-order unification -- most relevant unifiers and unification with case distinction
• Unification with extended patterns
• Unification of higher-order patterns in linear time and space

Cites work

• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 512797 (Why is no real title available?)
• scientific article; zbMATH DE number 1761899 (Why is no real title available?)
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A confluent reduction for the extensional typed \(\lambda\)-calculus with pairs, sums, recursion and terminal object
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Higher-order unification revisited: Complete sets of transformations
• The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
• The undecidability of the second-order unification problem
• The virtues of eta-expansion
• Unification with extended patterns

Cited in

(9)

• Two thoughts on higher-order unification -- most relevant unifiers and unification with case distinction
• Logic Programming
• Higher-order pattern complement and the strict \(\lambda\)-calculus
• Higher-order unification via combinators
• scientific article; zbMATH DE number 1303341 (Why is no real title available?)
• scientific article; zbMATH DE number 4068831 (Why is no real title available?)
• Higher-order dynamic pattern unification for dependent types and records
• Functions-as-constructors higher-order unification: extended pattern unification
• Optimizing higher-order pattern unification.

This page was built for publication: Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5055872)