문제

From pg. 35 of Lambda Calculus and Combinators An Introduction:

Corollary 3.3.1 in $\lambda$ and $CL$: for every $Z$ and $n \ge 0$, the equation

$$ xy_1 \ldots y_n = Z $$

can be solved for $x$. That is, there is a term $X$ such that

$$ Xy_1 \ldots y_n =_{\beta, w} [X/x]Z. $$

Proof: Choose $X \equiv \mathsf{Y} (\lambda x y_1 \ldots y_n.Z)$.

Note: In the book, we assume that $\mathsf{Y} \equiv (\lambda ux. xuux)(\lambda ux. xuux)$. Further, for ease of notation, let $V \equiv (\lambda x y_1 \ldots y_n.Z)$.

The problem is that when I check this with my own examples, I'm not getting this result.

For example, suppose that neither $x$ nor any of $y_1, \ldots , y_n$ is in the free variables of $Z$ (to make it easy). Then this theorem asserts that if $X \equiv \mathsf{Y}(\lambda x y_1 \ldots y_n . Z)$, then

$$ Xy_1 \ldots y_n =_{\beta, w} Z $$

When I check whether this true, I get

$$ (\mathsf{Y}(\lambda x y_1 \ldots y_n . Z))y_1 \ldots y_n = (\mathsf{Y}V)y_1 \ldots y_n = (V\mathsf{Y}V)y_1 \ldots y_n =_{\beta, w} Zy_n $$

Am I doing something wrong?

올바른 솔루션이 없습니다

라이센스 : CC-BY-SA ~와 함께 속성
제휴하지 않습니다 cs.stackexchange
scroll top