잔글 (→역사) |
잔글 (→람다 연산) |
||
| 1번째 줄: | 1번째 줄: | ||
=람다 | =람다 계산= | ||
{{학술}} | {{학술}} | ||
[[분류:람다 | [[분류:람다 계산]] | ||
{{넘겨주기 있음|람다 대수|람다 | {{넘겨주기 있음|람다 대수|람다 연산|람다 계산법|받침=예}} | ||
'''람다 | '''람다 계산'''(람다 대수, 람다 연산, 람다 계산법; {{llang|1=en|2=lambda calculus}})은 수리논리학과 이론 컴퓨터과학에서 사용하는 형식 체계(formal system)로, 함수의 정의, 적용, 재귀 등을 치환, 바인딩(binding) 등을 이용하여 추상화한다. [[알론조 처치]]가 1930년대 처음 발표하였다. | ||
== 역사 == | == 역사 == | ||
| 11번째 줄: | 11번째 줄: | ||
* 위의 언어로 서술된 모든 문제를 해결할 수 있는 방법을 찾아라. | * 위의 언어로 서술된 모든 문제를 해결할 수 있는 방법을 찾아라. | ||
첫 번째 것은, 만약 수학적인 문제만으로 제한한다면, [[러셀]]과 [[프레게]] 등에 의한 '집합론'의 공리적 서술로 인하여 꽤 만족스러운 결과를 얻었다고 할 수 있다. 하지만 두 번째 것은, 당연히 안 될 것 같지만, 그 증명이 명확하지 않았다. (이는 [[힐베르트]]에 의하여 ''Entscheidungsproblem''로 불리게 된다. 직역하면 ''결정 문제''이다.) 이것은 1930년대에 [[알론조 처치]]와 [[앨런 튜링]]에 의하여 각각 독립적으로 해결되는데, 그 답은 [[처치-튜링 명제]]를 가정할 때<ref>Church-Turing 명제는 다음을 말한다: 알고리듬으로 계산 가능함과 튜링 기계로의 계산 가능성은 동치이다. 이와 동치 명제로, 알고리듬으로 계산 가능함과 lambda calculus로 표현 가능함은 동치이다.)</ref> '''No'''이다. 튜링은 후에 이 두 방법으로의 ''계산 가능성'', 즉 계산 가능한 함수들의 모임이 서로 같음을 보였다. | 첫 번째 것은, 만약 수학적인 문제만으로 제한한다면, [[러셀]]과 [[프레게]] 등에 의한 '집합론'의 공리적 서술로 인하여 꽤 만족스러운 결과를 얻었다고 할 수 있다. 하지만 두 번째 것은, 당연히 안 될 것 같지만, 그 증명이 명확하지 않았다. (이는 [[힐베르트]]에 의하여 ''Entscheidungsproblem''로 불리게 된다. 직역하면 ''결정 문제''이다.) 이것은 1930년대에 [[알론조 처치]]와 [[앨런 튜링]]에 의하여 각각 독립적으로 해결되는데, 그 답은 [[처치-튜링 명제]]를 가정할 때<ref>Church-Turing 명제는 다음을 말한다: 알고리듬으로 계산 가능함과 튜링 기계로의 계산 가능성은 동치이다. 이와 동치 명제로, 알고리듬으로 계산 가능함과 lambda calculus로 표현 가능함은 동치이다.)</ref> '''No'''이다. 튜링은 후에 이 두 방법으로의 ''계산 가능성'', 즉 계산 가능한 함수들의 모임이 서로 같음을 보였다. | ||
람다 | 람다 계산이 고안된 이후로, 람다 연산에 기반한 ''함수 프로그래밍 언어''(functional programming language)가 만들어졌다. ''Reduction machine''은 이런 functional language의 실행을 위하여 고안되었다. | ||
== 이해 == | |||
Lambda calculus는 함수의 계산을 조금 더 간편하게 나타내는 표기이다. 간단히 말하면, 대수학에서 잊을 만하면 한 번씩 나오는 'evaluation'과 비슷한 개념이라고 할 수 있다. 예를 들어, <math>x</math>에 대한 식 <math>x^2 - \sin x</math>가 있다고 하자. 이는 다음과 같은 함수를 나타내기도 한다: | |||
:<math>x \mapsto x^2 - \sin x.</math> | |||
이 함수를 lambda calculus에서는 | |||
:<math>\lambda x.x \mapsto x^2 - \sin x</math> | |||
로 나타낸다.<ref><math>\lambda x[x \mapsto x^2 - \sin x]</math>로 나타내기도 한다.</ref> 그리고 이 함수의 <math>x=a</math>에서의 함숫값을 | |||
:<math>(\lambda x. x^2 - \sin x)a</math> | |||
로 나타낸다. 예를 들어 <math>(\lambda x.x^2 - \sin x)\pi = \pi^2 - \sin \pi = \pi^2</math>이다. 이 λ-연산자는 | |||
2016년 7월 10일 (일) 23:45 판
람다 계산
람다 계산(람다 대수, 람다 연산, 람다 계산법; 영어: lambda calculus)은 수리논리학과 이론 컴퓨터과학에서 사용하는 형식 체계(formal system)로, 함수의 정의, 적용, 재귀 등을 치환, 바인딩(binding) 등을 이용하여 추상화한다. 알론조 처치가 1930년대 처음 발표하였다.
역사
라이프니츠는 다음과 같은 생각을 가지고 있었다.
- 모든 문제들이 서술될 수 있는 '보편적인(universal) 언어'를 만들어라.
- 위의 언어로 서술된 모든 문제를 해결할 수 있는 방법을 찾아라.
첫 번째 것은, 만약 수학적인 문제만으로 제한한다면, 러셀과 프레게 등에 의한 '집합론'의 공리적 서술로 인하여 꽤 만족스러운 결과를 얻었다고 할 수 있다. 하지만 두 번째 것은, 당연히 안 될 것 같지만, 그 증명이 명확하지 않았다. (이는 힐베르트에 의하여 Entscheidungsproblem로 불리게 된다. 직역하면 결정 문제이다.) 이것은 1930년대에 알론조 처치와 앨런 튜링에 의하여 각각 독립적으로 해결되는데, 그 답은 처치-튜링 명제를 가정할 때[1] No이다. 튜링은 후에 이 두 방법으로의 계산 가능성, 즉 계산 가능한 함수들의 모임이 서로 같음을 보였다. 람다 계산이 고안된 이후로, 람다 연산에 기반한 함수 프로그래밍 언어(functional programming language)가 만들어졌다. Reduction machine은 이런 functional language의 실행을 위하여 고안되었다.
이해
Lambda calculus는 함수의 계산을 조금 더 간편하게 나타내는 표기이다. 간단히 말하면, 대수학에서 잊을 만하면 한 번씩 나오는 'evaluation'과 비슷한 개념이라고 할 수 있다. 예를 들어, [math]\displaystyle{ x }[/math]에 대한 식 [math]\displaystyle{ x^2 - \sin x }[/math]가 있다고 하자. 이는 다음과 같은 함수를 나타내기도 한다:
- [math]\displaystyle{ x \mapsto x^2 - \sin x. }[/math]
이 함수를 lambda calculus에서는
- [math]\displaystyle{ \lambda x.x \mapsto x^2 - \sin x }[/math]
로 나타낸다.[2] 그리고 이 함수의 [math]\displaystyle{ x=a }[/math]에서의 함숫값을
- [math]\displaystyle{ (\lambda x. x^2 - \sin x)a }[/math]
로 나타낸다. 예를 들어 [math]\displaystyle{ (\lambda x.x^2 - \sin x)\pi = \pi^2 - \sin \pi = \pi^2 }[/math]이다. 이 λ-연산자는