abstraction = binding free variable.
추상화,abstraction : to bind the free variable
$\displaystyle x$ in
$\displaystyle M.$
e.g.
$\displaystyle \lambda x.yx$
여기서
$\displaystyle x$ : bound_variable
$\displaystyle y$ : free_variable 임.
치환,substitution $\displaystyle [x:=N]$ 은 오로지 x의 free occurrences일 때만 수행된다.
("only performed in the free occurrences of x:")
$\displaystyle yx(\lambda x.x)[x:=N]\equiv yN(\lambda x.x)$
미적분학에서도 비슷한
variable_binding =,variable_binding =,variable_binding . variable_binding
이 있다.
$\displaystyle \int_a^b f(x,y)dx$ 에서 : $\displaystyle x$ is bound, $\displaystyle y$ is free.
It does not make sense to substitute 7 for
$\displaystyle x:$
$\displaystyle \int_a^b f(7,y)d7$
but substitution for
$\displaystyle y$ makes sense:
$\displaystyle \int_a^bf(x,7)dx$
위생(hygiene)의 이유로, 특정 식에서 일어나는
occurs bound variables는 항상 free variables와 다르다고 가정한다.
이것은 bound variables의 이름바꾸기
renaming을 통해 확실히 확인 가능
(...맞나? 혹은 '이름바꾸기를 해도 만족' 정도가 적당? can be fulfilled)하다.
e.g. λx.x becomes λy.y
다음 식도 마찬가지 방식.
(λx.x)a = a = (λy.y)a
사실 그들은 같은 algorithm을 표시한다
denote. 그래서 bound variables 이름만 다른
식,expressions들은 동일하다
are identified.