람다 대수 베타 축약

람다 대수 베타 축약

람다 대수의 베타 축약(Beta-reduction)은 람다 대수에서 함수 적용을 수행하는 과정입니다.
함수와 인자를 결합하여 하나의 표현식으로 줄이는 과정으로, 계산의 기본 단위를 나타냅니다.
베타 축약은 람다 대수의 핵심 연산으로, 프로그램의 실행을 모델링하는 방법을 제공합니다.

베타 축약은 다음과 같은 기본 규칙을 따릅니다.

(λx. E1) E2 → E1[x := E2]

이 규칙은 함수 (λx. E1)에 인자 E2를 적용하면 결과 표현식 E1[x := E2]가 생성된다는 것을 의미합니다.
여기서 E1[x := E2]는 표현식 E1에서 매개변수 x가 출현하는 모든 부분을 E2로 치환한 결과입니다.

실습

(λx. x + 1) 2

베타 축약을 적용하면 다음과 같이 계산할 수 있습니다.

(2 + 1) = 3

베타 축약은 계산을 수행하는 방법을 정의하며, 람다 대수에서 프로그램의 실행을 모델링합니다.
중첩된 함수 적용이나 람다 표현식이 포함된 복잡한 표현식도 베타 축약을 통해 단순한 형태로 축약되고, 최종 결과값으로 계산됩니다.