A (machine-oriented) logic based on pattern matching

摘要

Robinson’s unification algorithm can be identified as the underlying machinery of both C. Meredith’s ruleD (condensed detachment) in propositional logic and of the construction of principal types in lambda calculusand combinatory logic. In combinatory logic, it also plays a crucial role in the construction ofMeyer,Bunder Powers’ Fool’s model. This paper now considers pattern matching, the unidirectional variant ofunification, as a basis for logical inference, typing, and a very simple and natural model for untyped combinatorylogic. An analysis of the new typing scheme will enable us to characterize a large class of terms ofcombinatory logic which do not change their principal type when being weakly reduced.We also considerthe question whether the major or the minor premisse should be used as the fixed pattern.