람다 미적분의 감소

Question

나는 최근에 람다 계산법에 대해 연구 해왔고 나는 환원과 대체에 대해 많은 의구심을 가지고있다. 알파 및 베타 감소 란 무엇입니까? 그리고 언제 그리고 왜 사용됩니까?

누군가가 λ caculus의 축소 및 대체에 대한 훌륭한 자료를 말할 수 있다면 좋을 것입니다.

Answer 1

베타 감소는 람다 미적분 계산에서 계산에 사용되는 기본 적용 규칙입니다. 같이 그것은 대체를 통해 적용됩니다

당신은 람다 용어가 있다면 : (\ XX) 과 오른쪽에있는 일부 값 :

는 그런 다음 오른쪽에있는 모든 바운드 변수를 대체 할 y로 귀하의 람다 용어에 (.). 바운드 변수는 (.)의 왼쪽 변수와 일치하는 변수이므로이 경우 x입니다. Y는 람다 식 (X)의 모든 항목에 바인딩

The reduction would be of the form: 
(\x.x)y //y gets bound to all occurences of x to the right of the period 
y 

. 이것은 신원 기능입니다.

알파 "감소"는 보통 알파 등가 또는 알파 재 작성 규칙이라고합니다. 그들은 표현의 의미를 바꾸지 않고 람다 용어와 바운드 변수의 이름을 바꿀 수 있다고 말합니다.

예를 들어 위의 ID 함수를 사용하여 (\ j.j)와 같이 람다 용어를 쉽게 작성할 수 있습니다. 위키 피 디아 페이지가 꽤 상세한이지만, 표기 무겁고 몇 가지 좋은 다시 판독을 아마 필요하다 : 학습 자원으로

(\j.j)y //y gets bound to all occurrences of j to the right of the period 
y 

을 : 그것은 그림과 같이 우리의 응용 프로그램의 결과를 변경하지 않을 것입니다.

람다 미적분학 (lambda calculus)이 작동하는 방식에 대해 더 나은 직관력을 찾고 있다면 대부분의 컴퓨터 과학 부서에 슬라이드가 있습니다.

당신은 찾을 수

이 도움이 : http://www.classes.cs.uchicago.edu/archive/2002/winter/CS33600/slides/Lesson2.pdf https://www.utdallas.edu/~gupta/courses/apl/lambda.pdf