English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
  Local TagsRelease HistoryDetailsSummary

Released
Report

Unification and matching in Church's Original Lambda Calculus

MPS-Authors
/persons/resource/persons44660

Hustadt,  Ullrich
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

MPI-I-92-219.pdf
(Any fulltext), 141KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Hustadt, U.(1992). Unification and matching in Church's Original Lambda Calculus (MPI-I-92-219). Saarbrücken: Max-Planck-Institut für Informatik.


Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-B1CB-7
Abstract
In current implementations of higher-order logics higher-orderunification is used to lift the resolution principle from the first-order case to the higher-order case. Higher-order matching is the core of implementations of higher-order rewriting systems and some systems for program transformation. In this paper I argue that Church's original lambda calculus, called non-forgetful lambda calculus, is an appropriate basis for higher-order matching. I provide two correct and complete algorithms for unification in the non-forgetful lambda calculus. Finally, I show how these unification algorithms can be used for matching in the non-forgetful lambda calculus.