viewpoint: | combinatory logic | lambda calculus | |||
Enter a term to reduce (or click on one of the terms below): Example terms: |
Weak β-Reduction in λ-Calculus:
An occurrence of a β-redex R in a λ-term P is called weak in P iff no variable-occurrence free in R is bound in P. A weak reduction is one that consists only of weak contractions, that is, contractions of weak β-redexes. See: Çağman, N. and Hindley, J. R. 1998. Combinatory weak reduction in lambda calculus. Theor. Comput. Sci. 198, 1-2 (May. 1998), 239-247. |