람다 계산 베타 축소 계산기

(λx.M) N 형태의 식에서 M 안의 x를 전부 N으로 바꿔 넣는 계산 규칙입니다. 함수를 인자에 적용하는 것과 같은 뜻이며, 람다 계산의 유일한 계산 규칙입니다.

한 항에 축소 가능한 자리가 여럿 있을 때 가장 왼쪽·바깥쪽부터 축소하는 전략입니다. 표준화 정리에 따라 정규형이 존재한다면 정규 순서가 반드시 찾아냅니다 — 인자를 먼저 계산하는 다른 전략으로는 정규형이 있는데도 못 찾고 발산하는 경우가 있습니다.

치환하려는 값에 있는 자유변수 이름이 대상 항에서 묶인 변수 이름과 같을 때, 그냥 글자만 바꾸면 자유변수가 뜻하지 않게 묶여버립니다(변수 포획). 이를 막기 위해 묶인 변수를 새 이름으로 먼저 바꾼 뒤 치환합니다. 이 계산기는 이 과정을 자동으로 처리합니다.

네. (λx.x x)(λx.x x) 같은 식은 축소해도 축소해도 자기 자신으로 돌아와 영원히 정규형에 도달하지 않습니다. 람다 계산은 튜링 완전이라 정지 문제가 결정 불가능하므로, 이 계산기는 최대 스텝 수에 도달하면 실행을 강제로 멈춥니다.

아니요. 입력한 람다식과 계산 과정은 모두 브라우저에서만 처리되며 서버로 전송되지 않습니다.