Lambda Calculus
람다계산법은 함수 정의, 함수 응용, 재귀 (function definition, function application, recursion) 등을 조사하기 위해 설계된 형식 시스템이며 1930 연대에 Alonzo Church 와 Stephen Kleene 에 의해 소개되었다. Church 는 결정문제 (Entscheidungsproblem) 를 풀기위해 1936 년에 lambda calculus 를 사용했다. (그는 Entscheidungsproblem 의 해라고 할 만한 알고리즘이 존재하지 않는다고 증명했다). 람다 계산법은 계산가능한 함수 (computable function) 가 무엇인지를 명확히 정의하는데 사용될 수 있다. 두 개의 람다 계산 표현식이 같은 것인지에 대한 질문은 일반적인 알고리즘으로는 풀 수 없다. 이것은 결정될 수 없는 것 (undecidability) 은 증명될 수 없다 는 멈춤문제 (Halting Problem) 이전에는 최초의 질문이다. 람다계산법은 Lisp 과 같은 함수형 프로그램 언어에 큰 영향을 끼쳤다.... 여기서는 처치가 원래 착상한 untyped lambda calculus 를 다룬다. 그 이후 typed lambda calculi 가 개발되었고 여기서는 언급되지 않는다......... (Wikipedia : Lambda calculus)
...... 20 세기가 시작될 무렵, 수학자 David Hilbert 는 어떤 수학적인 명제가 입력으로 주어질 때 이의 참과 거짓을 알아내는 알고리즘을 찾고자 하는 일종의 `수학 자동화' 연구를 시작하였습니다. 그후 1931년에 이 방면의 연구에서의 금자탑이라고 할 수 있는 Kurt Gödel 의 논문이 발표되었습니다. 즉 그러한 알고리즘은 존재할 수 없음을 증명한 유명한 `불완전성 정리 (Incompleteness Theorem)' 를 발표한 것입니다. 그의 결과를 간단하게 설명하면, 모든 수학적인 논리 체계에는 그 논리 자체로써는 증명할 수 없는 참인 명제들이 존재한다는 것입니다........이렇게 일단 풀 수 없는 문제가 존재함이 증명된 후 많은 학자들은 풀 수 있는 문제들에 대한 연구에 몰두하여 여러가지 계산 모델들을 제안하였습니다. 그 예들로는 클레이너(Kleene)가 시작하고 쳐치(Church)가 많이 공헌한 재귀함수 (Recursive Function), 역시 Alonzo Church 의 람다계산법, Emil Post 의 포스트 시스템 (Post Systems), 또 Andrei Markop 의 마르코프 알고리즘 (Markov Algorithm), 그리고 전산학도들에게 가장 친숙한 Alan Turing의 튜링기계 (Turing Machine) 등이 있습니다. .......(인공지능과 컴퓨터의 한계 : 김도형 )
...... 이제 강력한 연산자인 추상화에 대해서 살펴보자. 이를 위해서 그리스 문자 λ (람다) 를 쓰고 그 바로 다음에 처치의 함수를 표시하는 변수 기호, 예를 들어 x 를 써 주는데 이 변수는 다만 '명목 변수 (dummy variable)' 역할을 한다. 그 바로 다음에 대괄호로 둘러싸인 식이 나오는데 그 식 안에 등장하는 모든 x 들은 식 바로 다음에 오는 것이 들어갈 수 있는 '빈 자리' 의 역할을 한다. 그러므로,
λx.[fx]
가 의미하는 것은 함수로서 만일 a 라는 값을 적용하면 fa 를 만들어 주는 함수이다. 즉,
(λx.[fx])a = fa
다시 말하면 λx.[fx] 는 단지 함수 f 를 의미할 따름이다. 즉,
λx.[fx] = f
........... 결국 1937 년에 처치와 튜링이 각자 독자적인 연구에 의해서 모든 계산 가능한 (알고리즘적인) 연산들, 즉 튜링 기게로 수행될 수 있는 연산들은 처치의 계산법에 의해서도 수행될 수 있고 그 역도 성립한다는 것이 밝혀졌다. ..... 이는 실로 놀라운 사실로서 이 결과로 인하여 계산가능성 이론 (Computability Theory) 이라는 개념이 근본적으로 객관적이고 수학적인 특성을 갖는다는 것이 설득력을 얻게 되었다. 처치의 방법에서 계산 가능성이라는 개념은 외형상 계산기와는 전혀 연관성이 없는 것처럼 보일지도 모른다. 그럼에도 불구하고 그것은 실생활의 계산과도 깊은 관계를 가지고 있다. 특히 강력하면서도 유연함을 자랑하는 컴퓨터 언어인 Lisp 는 본질적으로 처치의 람다 계산법의 기본 구조를 사용하고 있다. ......... 계산 가능성을 정의하는 데 다른 방법들도 있다 ........... (처치의 람다 계산법 : Roger Penrose)
.... ...... 컴퓨터 소프트웨어의 경우에도 그 의미하는 바를 표현하는 가장 좋은 방법은 수학을 이용하는 방법이다. 소프트웨어가 의미하는 바를 정확하게 집어낼 수 있으려면 그 소프트웨어의 코드가 의미하는 바, 예를 들면 코드가 수행하는 일 등을 명확하게 표현할 수 있어야 한다. 그 표현으로부터 새로운 이론 및 사실을 끌어낼 수 있다면 더 좋을 것이다. 자연 과학에서처럼 이러한 것을 가능하게 하는 것은 바로 수학이다. 컴퓨터 과학에서도 소프트웨어의 의미하는 바를 정확하게 수학적으로 표현하기 위해 많은 모델이 연구되고 있다 ..... 소프트웨어가 의미하는 바를 수학적으로 표현한 모델의 하나로 람다 계산법(Lambda Calculus)이 있다. 어떤 소프트웨어가 하는 일은 무언가를 계산하는 것이라는 관점에서 살펴 볼 수 있다. 람다 계산법은 이 계산이라는 것을 수학적으로 표현한 것이다. 람다 계산법은 현재까지 알려진 직관적으로 계산 가능한 모든 것들을 표현할 수 있으며 따라서 모든 소프트웨어가 계산하는 과정을 이것을 이용하여 표현할 수 있다. 이 람다 계산법을 확장하여 계산이라는 과정 중에서 일어나는 자료의 형이 올바른 것인지를 판단할 수 있도록 타입이라는 개념을 추가한 타입을 갖는 람다 계산법(Typed Lambda Calculus)도 있다 ...... 그러나 아직 소프트웨어가 의미하는 바를 물리학이 자연 현상이 일어나는 원인을 수학적으로 설명하듯 명쾌하게 설명하고 있는 것 같지는 않다. 소프트웨어가 의미하는 바는 완벽하게 알려면 그 소프트웨어가 돌아가는 기계, 사용되는 환경 등 그 관점에 따라 매우 다양하고 복잡할 수가 있기 때문에 어떤 프로그램이 의미하는 바를 수학적으로 완벽하게 표현한다는 것은 사실은 인간이 생각할 수 있는 것을 수학적으로 표현하는 작업만큼 어려울 지도 모른다. 그렇지만 이러한 것이 이루어진다면 프로그래밍 기법과 그것을 이용한 소프트웨어는 지금과는 차원이 다르게 발전할 수 있으리라고 생각한다. ...... (컴퓨터 소프트웨어의 수학적 의미 : 배경민)
term :
람다 계산법 (Lambda Calculus) 처치-튜링 명제 (Church-Turing Thesis) Alan Turing Alonzo Church 튜링기계 (Turing Machine) 계산가능성 이론 (Computability Theory) 계산 (Computation) 마르코프 알고리즘 (Markov Algorithm) 재귀함수 (Recursive Function) 포스트 시스템 (Post Systems) 결정문제 (Entscheidungsproblem)
video :
컴퓨터과학이 여는 세계 - 언어의 중력과 람다계산법의 정의 : SNU : 이광근 : 2016/03/07 ... 동영상 82개