아는 사람 없냐?

기본식 (람다x M)N -> M[x<-N]

의 의미가 M식에 있는 모든 변수 x를 N으로 바꿔라... 한마디로 N이 인수고 x가 매개변수라는거자나

근데 (람다x (zx))[x<-y]같은 경우

x가 zx에 묶여 있고 인자N이 없으므로 N에는 자유로운 변수 x를 왜 u로 치환하고

그럼 (람다u (zu))[x<-y] = (람다u (zu))가 되는거야?

뭐 이걸 베타축약이라고 한다는데 걍 이렇게 두 단계(??)로 되어있으면 u로 바꾸고 뒤에꺼 없에기만 하면 되나?

뭐 이해를 하고 넘어가야겠는데.....설명 잘 해줄 플갤러 없음?