"더하기" 곱하기 "더하기"는?

이 영상은 모든 것을 함수로 정의하고 계산하는 체계인 람다 대수(Lambda Calculus) 의 기초부터 심화 개념까지 다룹니다. 계산의 본질과 알론조 처치의 공헌, 그리고 현대 프로그래밍 언어의 뿌리가 된 논리적 구조를 시각적으로 설명합니다.

서론: 순수 계산의 세계

• 화면상의 복잡한 선들은 순수 계산의 과정을 나타냅니다.
• 이는 대수적 조작이나 불 논리와는 다른 영역의 연산입니다.
• 예시로 3 팩토리얼(3!) 을 평가하면 결과값 6이 도출됩니다.
• 람다 대수에서 이 기괴한 선들은 각각 특정 의미를 가집니다.
  • 분홍색 부분: 팩토리얼 함수를 상징합니다.
  • 노란색 부분: 숫자 3을 상징합니다.
  • 파란색 부분: 함수를 숫자에 적용하는 행위를 상징합니다.
• 람다 대수의 마법은 특정 식이 숫자 인지, 숫자에 작용하는 함수인지, 아니면 다른 것인지 즉각적으로 알 수 없다는 점에 있습니다.
• 이 언어에서는 숫자와 함수 사이에 구분이 존재하지 않습니다.
• 함수 적용(Function Application) 을 통해 팩토리얼을 3에 적용할 수 있는 것처럼, 3을 팩토리얼에 적용하는 것도 가능합니다.
• 람다 대수를 이해하기 위해서는 함수, 프로그램, 값, 데이터 타입에 대한 기존 개념을 완전히 잊어야 합니다.

제1장: 람다의 길(The Way of the Lambda)

• 계산(Computation) 의 본질에 대한 탐구는 1900년대 수학자 데이비드 힐베르트로부터 시작되었습니다.
• 그는 임의의 수학적 정리가 참인지 거짓인지 판별할 수 있는 알고리즘(절차) 이 있는지 물었습니다.
• 세 명의 인물이 이 질문에 서로 다른 방식으로 답하며 컴퓨터 과학의 기초를 닦았습니다.
  • 알론조 처치: 람다 대수를 발명하고 함수형 프로그래밍 패러다임을 창시했습니다.
  • 앨런 튜링: 튜링 기계를 발명하고 명령형 프로그래밍의 기반을 마련했습니다.
  • 쿠르트 괴델: 일반 재귀 함수를 발명하고 불완전성 정리를 증명했습니다.
• 이들의 아이디어는 힐베르트의 과제가 불가능함을 증명했고, 현대 프로그래밍 언어의 근간이 되었습니다.
• 람다 대수는 본질적으로 기호 문자열(Strings of symbols) 을 조작하는 시스템입니다.
• 람다 대수의 문자열은 괄호, 알파벳 문자, 람다($\lambda$)와 점(.)의 조합으로 구성됩니다.
• 람다 식을 구성하는 세 가지 템플릿은 다음과 같습니다.
  1. 변수: $a, x, y$ 등 알파벳 문자 그 자체입니다.
  2. 함수 정의(추상화) : $(\lambda a. \_)$ 형태입니다. $a$는 입력 변수의 이름이며, 빈칸은 함수의 본체입니다.
  3. 함수 적용: $(\_ \_)$ 형태입니다. 왼쪽은 함수, 오른쪽은 인자(Argument)를 의미합니다.
• 이 템플릿들을 조합하여 무수히 많은 유효한 람다 식을 생성할 수 있습니다.

제2장: 트롬프의 도표(Tromp's Diagrams)

• 존 트롬프가 고안한 도표를 사용하면 복잡한 람다 식을 시각화할 수 있습니다.
• 도표의 구성 요소는 식의 구성 요소와 일대일로 대응됩니다.
  • 수직선: 변수를 나타냅니다.
  • 상단의 수평 바: 람다 추상화(함수 정의)를 나타냅니다.
  • 하단의 분기 구조: 함수 적용을 나타냅니다.
• 변수를 나타내는 수직선은 자신을 묶고 있는(Bind) 상단의 수평 바에 연결됩니다.
• 가장 바깥쪽의 함수 적용은 도표 전체를 감싸는 구조로 표현됩니다.

제3장: 베타 축약(Beta Reduction)

• 람다 식을 평가하는 과정을 베타 축약($\beta$-Reduction) 이라고 합니다.
• 이는 함수의 입력 변수를 실제 인자 값으로 교체하는 행위입니다.
• 축약의 단계는 다음과 같습니다.
  1. 람다 기호 뒤에 명시된 묶인 변수를 식별합니다.
  2. 함수 본체 내부에서 해당 변수의 모든 사례를 찾습니다.
  3. 기존의 함수 정의 구조와 외부 괄호를 제거합니다.
  4. 식별된 변수 자리에 입력으로 들어온 인자 값을 대입합니다.
• 이는 일반적인 대수학에서 함수 $f(x)$에 특정 값을 대입하여 계산하는 방식과 동일합니다.
• 도표상에서도 인자 값이 변수의 위치를 차지하고 연결 구조가 재편되는 과정으로 시각화됩니다.
• 이 과정은 식의 가장 윗 단계뿐만 아니라 내부의 하위 구성 요소에서도 발생할 수 있습니다.

제4장: 커링(Currying)

• 람다 대수의 엄격한 규칙상 함수 정의 시 람다($\lambda$)와 점(.) 사이에는 오직 하나의 문자(인자) 만 올 수 있습니다.
• 여러 개의 변수를 가진 함수를 만들기 위해 함수가 또 다른 함수를 반환하게 만드는 기법을 커링(Currying) 이라고 합니다.
• 예를 들어, 두 개의 인자를 받는 함수는 '첫 번째 인자를 받아, 두 번째 인자를 받는 또 다른 함수를 결과로 내놓는 함수'가 됩니다.
• $\lambda xy. \text{본체}$와 같은 표기법은 $\lambda x. (\lambda y. \text{본체})$의 축약형(Shorthand)으로 허용됩니다.

제5장: 불리언 산술(Boolean Arithmetic)

• 람다 대수에서는 참과 거짓 같은 논리값도 함수로 표현합니다.
• TRUE: $\lambda ab. a$ (두 개의 인자 중 첫 번째를 선택하는 함수).
• FALSE: $\lambda ab. b$ (두 개의 인자 중 두 번째를 선택하는 함수).
• 이러한 논리값 정의를 바탕으로 IF-THEN-ELSE 구조를 구현할 수 있습니다.
• 기본 논리 게이트의 구현 예시는 다음과 같습니다.
  • NOT: $\lambda x. (x \text{ FALSE TRUE})$ 형태입니다. $x$가 참이면 거짓을, 거짓이면 참을 선택합니다.
  • AND: $\lambda xy. (x y \text{ FALSE})$ 형태입니다. $x$가 참이면 $y$의 결과를 따르고, $x$가 거짓이면 무조건 거짓을 선택합니다.

제6장: 처치 수(Church Numerals)

• 숫자 또한 함수를 반복 적용하는 횟수로 정의됩니다.
• 0: 함수를 0번 적용하는 함수 ($\lambda f x. x$).
• 1: 함수를 1번 적용하는 함수 ($\lambda f x. f x$).
• 2: 함수를 2번 적용하는 함수 ($\lambda f x. f(f x)$).
• 숫자 $n$은 함수 $f$와 변수 $x$를 받아 $f$를 $x$에 $n$번 적용하는 구조를 가집니다.
• 기본적인 수학 연산의 정의는 다음과 같습니다.
  • SUCC(후속자 함수) : 숫자 $n$을 받아 함수 적용을 한 번 더 추가하여 $n+1$을 만듭니다.
  • 덧셈: 숫자 $n$에 후속자 함수를 $m$번 적용함으로써 $n+m$을 구현합니다.
  • 곱셈: 반복적인 덧셈이나 함수의 중첩 구조를 통해 정의합니다.
  • 거듭제곱: 함수 적용 횟수를 기하급수적으로 늘려 구현합니다.

제7장: 재귀(Recursion)

• 람다 대수 식은 고유한 이름을 가질 수 없으므로 식 내부에서 자기 자신을 직접 호출하는 재귀가 불가능해 보입니다.
• 이를 해결하기 위해 고정점 결합자(Fixed-point Combinator) 라는 특수한 식을 사용합니다.
• 튜링의 고정점 결합자($\Theta$) 는 임의의 함수 $F$에 대해 $\Theta F$가 $F(\Theta F)$와 베타 축약 관점에서 동일하게 작동하도록 만듭니다.
• 람다 대수의 모든 함수는 고정점을 가지며, 이를 통해 팩토리얼 같은 재귀 함수를 유한한 길이의 식으로 정의할 수 있습니다.
• 팩토리얼 함수 정의 단계:
  1. 재귀 호출이 필요한 자리를 변수 $f$로 둔 고차 함수를 만듭니다.
  2. 이 함수에 고정점 결합자를 적용하여 고정점을 찾습니다.
  3. 결과적으로 이름 없이도 자기 자신을 무한히 확장하며 계산하는 재귀 식이 완성됩니다.

제8장: 축약 그래프(Reduction Graphs)

• 하나의 람다 식은 축약할 수 있는 부분이 여러 곳일 수 있어 다양한 축약 경로가 존재합니다.
• 더 이상 축약할 수 없는 최종 상태를 베타 노멀 폼(Beta Normal Form) 이라고 부릅니다.
• 처치-로서 정리(Church-Rosser Theorem) : 어떤 경로로 축약하든 도달하는 최종 노멀 폼은 항상 동일합니다.
• 그러나 모든 식의 경로가 노멀 폼으로 이어지는 것은 아닙니다.
  • $\Omega_3$: 축약할수록 식의 크기가 무한히 커지는 식입니다.
  • $PP$: 축약하면 자기 자신으로 되돌아와서 상태 변화가 없는 식입니다.
• 팩토리얼 같은 복잡한 식은 축약 순서에 따라 정답에 도달하거나 혹은 무한 루프에 빠질 수도 있습니다.

제9장: 기초를 넘어서

• 처치-튜링 명제: 람다 대수는 현대의 어떤 컴퓨터가 할 수 있는 계산도 수행할 수 있을 만큼 강력합니다.
• 타입 람다 대수(Typed Lambda Calculus) : 변수에 데이터 타입을 할당하여 프로그램의 안정성을 높이는 분야입니다.
• 커리-하워드 대응: 수학적 증명과 컴퓨터 프로그램이 구조적으로 동일하다는 원리입니다. 프로그램을 작성하는 행위 자체가 정리를 증명하는 것과 같습니다.
• 현대 프로그래밍 언어와의 관계:
  • Lisp, Haskell 등은 람다 대수를 직접적인 기반으로 삼습니다.
  • Python, Rust, C++ 등 현대 언어들도 익명 함수인 람다(Lambda) 기능을 제공합니다.
• 람다 대수는 단순한 계산 도구를 넘어 정보의 구조와 계산의 본질에 대한 심오한 철학적 통찰을 제공합니다.