Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10325551 | Journal of Symbolic Computation | 2005 | 50 Pages |
Abstract
It is shown that unifiability of terms in the simply typed lambda calculus with β and η rules becomes decidable if there is a bound on the number of bound variables and lambdas in a unifier in η-expanded β-normal form.
Related Topics
Physical Sciences and Engineering
Computer Science
Artificial Intelligence
Authors
Manfred Schmidt-SchauÃ, Klaus U. Schulz,