[프로그래밍 언어론] 3. 프로그래밍 패러다임

1. 함수형 프로그래밍 언어

대부분의 전통적인 언어(Fortran, C, Java 등)는 폰 노이만 구조를 따른다. 

- 메모리(변수)와 연산이 분리되어 있다. 

- 상태(state)가 프로그램의 핵심 구성 요소

- 명령 순서에 따라 동작이 달라질 수 있다. 

 

폰 노이만 구조의 문제점

- 명령 중심 + 상태 기반 → 디버깅 어려움

- 부작용(side effects) → 추론 불가능성 증가

- 데이터 전송 병목 현상 → 속도 저하

 

그래서 등장한 대안이 함수형 프로그래밍(FP) 이다. 

 

수학함수

: 수학 함수는 항상 같은 입력과 같은 출력을 나타내는 순수 함수 (pure function)이다. 

함수는 매개변수와 인수만 사용하고, 부작용이 없고, 참조투명성을 가진다. 

이러한 수학함수의 순수성을 프로그래밍에 도입한 것이 함수형 프로그래밍의 출발점이다. 

 

John Backus의 함수형 프로그래밍 시스템 제안

- 변수 없는 프로그래밍

- 함수 조합만으로 프로그램 구성

- 수학적 속성을 활용한 프로그램 변환

- 계층적 프로그램 구조

: 표현의 자유 + 수학적 명확성을 강조한 함수형 프로그래밍 시스템의 기초가 된다.

 

함수형 프로그래밍(FP)의 주요 원리

- 고차함수(다른 함수를 인자로 받는 함수): 함수가 계속해서 함수를 호출할 때 발생하는 문제 해결

- 불변성: 데이터 구조는 불변

- 순수함수, 참조투명성

 

2. 병합정렬: Scheme - 함수형 프로그래밍

문법요약

- define: 변수/함수 정의

- if: 조건 분기

- null?, car, cdr, cons: 리스트 조작

 

merge 함수 

(define (merge L M)
  (if (null? L) M
      (if (null? M) L
          (if (< (car L) (car M))
              (cons (car L) (merge (cdr L) M))
              (cons (car M) (merge (cdr M) L)))))

 

split 함수 

(define (odd L)
  (if (null? L) '()
      (if (null? (cdr L)) (list (car L))
          (cons (car L) (odd (cddr L))))))

(define (even L)
  (if (null? L) '()
      (if (null? (cdr L)) '()
          (cons (cadr L) (even (cddr L))))))

(define (split L)
  (cons (odd L) (cons (even L) '())))

 

 mergesort 함수

(define (mergesort L)
  (if (null? L) L
      (if (null? (cdr L)) L
          (merge (mergesort (car (split L)))
                 (mergesort (cadr (split L)))))))

 

3. 병합정렬: Java vs Kotlin 

Java

- 명령형 스타일, 변수 사용 많다.

- 재귀는 가능하지만 문법구조는 복잡

- 참조 불변성 불만족

Java

 

Kotlin

- 고차 함수, 불변 리스트, When문 -> 함수형 스타일에 근접

- 코드 간결 + 추론 가능한 흐름 제공

- return 값 없다 : 불변성을 담보하기 때문에 Null 못쓰고, return값 없어도 return 한다.

Kotlin

FP를 제외한 언어들은 절대 재귀를 쓸 수 없다..

 

4. 꼬리재귀 최적화

TCO(Tail Call Optimication, 꼬리 호출 최적화)

: 특정함수가 다른 함수에 대한 호출을 수행할 때, 그 호출이 '꼬리 위치'에 이쓰면 별도의 스택 프레임을 쌓지 않고 기존 프레임을 재사용하여 실행하는 최적화이다. 

Java는 TCO 지원x

- 장점: 스택오버플로우 방지, 반복 방식과 비슷한 성능 제공

- 제약조건: 함수의 마지막 동작이 함수 호출, 호출 후 더 이상의 작업 x

 

TRE(Tail Recursion Elimination, 꼬리 재귀 제거)

: 꼬리호출 중에서도 자기 자신을 재귀 호출하는 경우에만 특화된 최적화 기법

- 자기 재귀 호출을 반복문(loop)으로 전환하여 재귀 호출 자체를 제거

 

5. 정리 증명

= 형식검증(Formal Verification)

: 소프트웨어나 수학 명제가 정확히 원하는 대로 작동함을 논리적으로 입증하는 과정

- 소프트웨어가 정의된 사양을 충족하는지 검증

- 오류 없는 시스템 설계

 

주요 접근 방식

- 자동 증명 (Automated Theorem Proving): SMT/SAT Solver 기반, 자동 추론

- 대화형 증명 (Interactive Theorem Proving): 인간이 증명 절차를 구성하고 도구가 검증한다.

 

6. Lean 언어

: 정리 증명 + 함수형 언어

Lean은 정리 증명기이자 함수형 언어로 아래의 특징을 가진다.

- 의존 타입 시스템 기반으로 매우 정밀한 표현 가능

- 함수형 언어의 특성: 불변성, 고차함수, 순수함수

- 수학적 정리 뿐만 아니라 소프트웨어 검증에도 활용 가능

 

논리 증명 예시 (AND 연산의 교환 법칙)

theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=
  fun hpq : p ∧ q =>
  have hp : p := And.left hpq
  have hq : q := And.right hpq
  show q ∧ p from And.intro hq hp

 

 

데이터 구조 예시: Binary Search Tree 정의

inductive Tree (β : Type) where
  | leaf : Tree β
  | node : Tree β → Nat → β → Tree β → Tree β

 

Lean은 프로그래밍과 증명의 경계를 허무는 도구로, 수학적 사고와 소프트웨어 안정성을 동시에 제공한다.