[Programming Languages #1] 프로그래밍 언어는 무엇을 배우는 학문인가?
Programming Languages 시리즈 1편 – 프로그래밍 언어를 정의하는 방법: Inductive Definition, Syntax, Semantics, Inference Rules
프로그래밍 언어를 배운다는 것은 무엇인가
“프로그래밍 언어를 공부한다”고 하면 보통 이렇게 생각한다.
- 새로운 문법을 익히고
- 라이브러리를 배우고
- 코드를 더 잘 짜는 것
하지만 이 시리즈에서 말하는 Programming Languages (PL) 는
조금 다른 질문에서 출발한다.
“프로그래밍 언어는 어떻게 만들어지고, 어떻게 동작하는가?”
우리가 보통 배우는 것 vs PL에서 배우는 것
일반적인 프로그래밍 학습은 이런 흐름이다.
- Python, C++, Java 같은 언어를 배우고
- 기능을 익히고
- 실제 문제를 푼다
하지만 PL에서는 이렇게 묻는다.
- 이 언어의 문법은 어떻게 정의되는가?
- 이 프로그램의 의미는 무엇인가?
- 이 코드는 왜 이렇게 실행되는가?
즉,
“사용하는 것”이 아니라 “이해하고 정의하는 것”이 목표다
핵심 관점: 프로그램을 ‘수학적 대상’으로 본다
PL에서 가장 중요한 전환은 이것이다.
프로그램을 코드가 아니라 “형식적인 객체”로 본다
예를 들어, 다음과 같은 프로그램이 있다고 하자.
1
2
3
let rec fact n =
if n = 0 then 1
else fact (n - 1) * n
이 코드를 단순히 “팩토리얼 함수”로 보는 것이 아니라,
PL에서는 이렇게 본다.
- 입력 → 프로그램 → 결과
즉, 프로그램은 하나의 변환 함수처럼 취급된다.
그래서 무엇을 하게 되는가
이 관점에서 보면 자연스럽게 두 가지 중요한 작업이 등장한다.
1) Interpreter
프로그램을 실행하는 규칙을 정의한다.
\[\text{Program} \rightarrow \text{Interpreter} \rightarrow \text{Result}\]즉,
“이 프로그램이 실제로 어떻게 계산되는가?”
를 명확하게 설명하는 것이다.
2) Type Checker
프로그램이 안전한지 검사한다.
\[\text{Program} \rightarrow \text{Type Checker} \rightarrow \text{Safe / Unsafe}\]즉,
“이 프로그램이 실행해도 문제가 없는가?”
를 판단한다.
왜 이게 중요한가
이 접근이 중요한 이유는 명확하다.
우리는 단순히 코드를 작성하는 것을 넘어서
다음과 같은 문제를 다루고 싶기 때문이다.
- 프로그램이 항상 올바르게 동작하는가
- 특정 오류가 절대 발생하지 않는가
- 코드의 의미를 정확하게 정의할 수 있는가
이런 질문은 직관이나 경험으로는 답할 수 없다.
그래서 필요해지는 것이 바로 형식적 사고(Formal reasoning) 다.
한 줄 정리
\[\text{Programming Languages} = \text{프로그램을 정의하고 이해하는 방법}\]Inductive Definition — 프로그램을 “정의하는” 방법
그렇다면,
“프로그램을 정의한다는 건 정확히 무슨 의미일까?”
이 질문에 답하기 위해 등장하는 핵심 개념이 바로
Inductive Definition (귀납적 정의) 다.
왜 이런 게 필요한가
프로그래밍 언어를 다루다 보면 이런 대상들을 계속 만나게 된다.
- 프로그램 (expression)
- 리스트, 트리 같은 자료구조
- 문법 (syntax)
이들은 모두 크기가 무한할 수 있다
예를 들어 아래와 같은 프로그램을 생각해보자.
1
2
3
4
5
x
x + 1
(x + 1) * (x + 2)
(x + (x + 1)) * ((x + 2) + 3)
...
“이 무한한 집합을 어떻게 정의할까?”
핵심 아이디어: 자기 자신으로 정의한다
Inductive Definition의 핵심은 한 문장이다.
“집합을 자기 자신을 이용해서 정의한다”
즉,
- 작은 것부터 시작하고
- 규칙을 이용해 점점 큰 것을 만든다
가장 간단한 예시
자연수 집합을 생각해보자.
다음처럼 정의할 수 있다.
- \(0\)은 자연수다
- \(n\)이 자연수면 \(n+1\)도 자연수다
이 두 줄만으로 우리는 무한한 집합을 정의했다.
\[\{0, 1, 2, 3, \dots\}\]프로그래밍 언어에서의 예시
이제 PL 관점에서 더 중요한 예시를 보자.
리스트 정의
리스트는 다음 두 규칙으로 정의할 수 있다.
- 빈 리스트 \([]\) 는 리스트다
- 어떤 값 \(x\) 와 리스트 \(xs\) 가 있으면,
\(x :: xs\) 도 리스트다
이 두 규칙으로 모든 리스트가 만들어진다.
여기서 \(x :: xs\) 는 조금 낯설 수 있는데,
이건 다음 의미를 가진다.
“값 \(x\) 를 리스트 \(xs\) 앞에 붙인다”
즉,
- \(x\): 하나의 값
- \(xs\): 리스트 (여러 개의 값)
(참고: 이 표기법은 함수형 언어(예: OCaml, Haskell)에서 자주 사용된다)
예를 들어:
1
2
3
1 :: [] = [1]
2 :: [1] = [2, 1]
3 :: [2, 1] = [3, 2, 1]
이렇게 “앞에 붙이는 연산”을 반복해서 리스트를 만든다.
따라서
\[[1,2,3] = 1 :: (2 :: (3 :: []))\]처럼 모든 리스트를 이 규칙으로 표현할 수 있다.
트리 정의
트리도 똑같다.
- 빈 트리는 트리다
- 두 개의 트리를 자식으로 가지면 트리다
즉, 복잡한 구조도
간단한 규칙 몇 개로 정의할 수 있다.
중요한 감각
여기서 꼭 잡아야 할 감각이 있다.
“만드는 규칙 = 정의”
즉 Inductive Definition은 단순한 설명이 아니라
구성 방법 자체를 정의하는 것이다.
세 가지 방식
귀납적 정의는 세 가지 방식으로 설명할 수 있다.
1) Top-down
- “이 값이 집합에 속하려면?”을 기준으로 정의
2) Bottom-up
- 작은 것부터 생성해서 집합을 구성
3) Inference Rules (가장 중요)
- 규칙 형태로 정의
PL에서는 대부분 이 세 번째 방식을 사용한다.
이 개념이 중요한 이유는 단순하다.
프로그래밍 언어의 모든 것이 이 방식으로 정의되기 때문이다
- 문법 (syntax)
- 의미 (semantics)
- 타입 시스템 (type system)
전부 다 귀납적으로 정의된다.
이 방식이 이후 모든 내용의 핵심이 되기 때문에,
아래 섹션에서 조금 있다가 더 자세히 살펴보겠다.
SyGuS와 연결되는 포인트
여기서 중요한 연결이 하나 나온다.
우리가 앞에서 본 Grammar를 떠올려보자.
\[S \rightarrow x \mid S + S \mid 1\]이건 사실 무엇인가?
Inductive Definition이다
- base case: \(x, 1\)
- recursive case: \(S + S\)
즉,
Grammar = 프로그램의 귀납적 정의
한 줄 정리
\[\text{Inductive Definition} = \text{유한한 규칙으로 무한한 구조를 정의하는 방법}\]Syntax vs Semantics — 프로그램의 “형태”와 “의미”
Inductive Definition을 통해 우리는
프로그램을 어떻게 정의하는지 알게 되었다.
이제 다음 질문이 자연스럽게 나온다.
“그렇게 정의된 프로그램은 무엇을 의미하는가?”
이 질문에 답하기 위해 등장하는 두 개념이 바로
- Syntax (문법)
- Semantics (의미)
이다.
Syntax — 프로그램의 “모양”
Syntax는 프로그램이 어떻게 생겼는지를 다룬다.
즉,
“이게 문법적으로 올바른 프로그램인가?”
를 판단하는 기준이다.
예시
다음 두 식을 보자.
1
x + 1
1
+ x 1
첫 번째 식은 우리가 사용하는 일반적인 문법에서는 올바르다.
두 번째 식은 보통의 언어에서는 문법 오류다.
즉,
- 첫 번째 식 → valid syntax
- 두 번째 식 → invalid syntax
Syntax는 어떻게 정의되는가
Syntax는 바로 우리가 앞에서 본 방식으로 정의된다.
\[S \rightarrow x \mid S + S \mid 1\]이건 단순한 규칙이 아니라,
“어떤 문자열이 프로그램인지”를 정의하는 것
이다.
즉,
Syntax = 프로그램의 집합을 정의하는 규칙
Semantics — 프로그램의 “의미”
이제 더 중요한 질문이다.
1
x + 1
이건 문법적으로 맞다.
그럼 이제 질문은 바뀐다.
“그래서 이건 무엇을 의미하는가?”
이걸 정의하는 것이 바로 Semantics다.
가장 직관적인 의미: 계산 결과
예를 들어 다음 식을 보자.
\[x = 3\]그럼
\[x + 1 = 4\]이건 프로그램의 가장 기본적인 의미다.
즉,
Semantics = 프로그램이 무엇으로 계산되는가
더 일반적으로 보면
Semantics는 다음과 같이 표현할 수 있다.
\[\text{Program} \rightarrow \text{Meaning}\]또는 더 구체적으로는:
\[\text{Program} \rightarrow \text{Value}\]즉, 프로그램은 어떤 결과로 “해석”된다.
Syntax vs Semantics 한 번에 보기
이 둘의 차이는 매우 중요하다.
| 구분 | 의미 |
|---|---|
| Syntax | 프로그램이 어떻게 생겼는가 |
| Semantics | 프로그램이 무엇을 의미하는가 |
직관적으로 보면
- Syntax → 문장이 맞는 문장인가
- Semantics → 그 문장이 무슨 뜻인가
왜 이 구분이 중요한가
이 구분이 중요한 이유는 단순하다.
문법이 맞다고 해서 의미가 항상 올바른 것은 아니다
예를 들어:
1
1 / 0
이건 Syntax적으로는 완전히 올바르다.
하지만 의미적으로는 문제가 있다.
또 다른 예:
1
x + y
Syntax는 문제 없다.
하지만 \(x, y\) 값이 없다면 의미를 계산할 수 없다.
즉,
- Syntax → 구조적 올바름
- Semantics → 실제 의미
이 둘은 완전히 다른 층위의 문제다.
Programming Languages에서의 핵심
PL에서는 이 둘을 명확하게 분리해서 다룬다.
- Syntax는 Grammar로 정의하고
- Semantics는 수학적으로 정의한다
이렇게 해야만
- 프로그램을 정확하게 분석하고
- 자동으로 검증하고
- 나중에 합성까지 가능해진다
한 줄 정리
\[\text{Syntax} = \text{형태}, \quad \text{Semantics} = \text{의미}\]Inference Rules — 규칙으로 정의하는 방법
Inductive Definition에서 우리는
“작은 규칙으로 큰 구조를 만든다”는 아이디어를 봤다.
이걸 더 정확하게 표현하는 방식이 바로 Inference Rule이다.
Inference rule은 다음 형태를 가진다.
\[\frac{A}{B}\]의미는 단순하다.
A가 참이면 B도 참이다
가정이 없는 경우는 특별하다.
\[\frac{}{B}\]이건 “항상 참인 기본 사실 (axiom)”이다.
예를 들어 자연수 집합은 다음 두 규칙으로 정의된다.
\[\frac{}{0 \in S} \qquad \frac{n \in S}{n+1 \in S}\]이 규칙의 의미는 명확하다.
- 0은 기본적으로 포함된다
- 포함된 값에서 계속 확장된다
중요한 점은 이것이다.
이 규칙으로 만들어낼 수 있는 것만 집합에 속한다
이제 이 규칙을 실제로 적용하는 과정을 보자.
이 과정을 Derivation (유도) 라고 한다.
예를 들어 3이 자연수임을 보이려면:
\[0 \in S \Rightarrow 1 \in S \Rightarrow 2 \in S \Rightarrow 3 \in S\]즉,
만들 수 있으면 포함된다
이 과정을 구조로 보면 Derivation Tree가 된다.
1
2
3
4
5
6
7
0 ∈ S
↓
1 ∈ S
↓
2 ∈ S
↓
3 ∈ S
- 시작: axiom
- 끝: 우리가 보이려는 결과
즉 이 트리는
“왜 이 값이 포함되는지”를 설명하는 증명 구조다
여기서 중요한 연결이 하나 나온다.
이 규칙들은 단순한 수학적 장난이 아니라,
프로그래밍 언어의 의미를 정의하는 데 그대로 사용된다
나중에는 다음과 같은 형태가 등장한다.
\[\rho \vdash e \Rightarrow v\]이건 이렇게 읽는다.
- 환경 \(\rho\)에서
- 프로그램 \(e\)는
- 값 \(v\)로 평가된다
즉,
Inference Rule = 프로그램의 실행 규칙
한 줄 정리
\[\text{Inference Rules} = \text{규칙으로 정의하고, 유도로 의미를 결정하는 방법}\]마무리
이번 글에서는 프로그래밍 언어를 바라보는 가장 기본적인 관점을 정리했다.
핵심은 하나다.
프로그램은 단순한 코드가 아니라, 형식적으로 정의되는 대상이다
이 관점에서 우리는 다음을 차례로 보았다.
Inductive Definition
→ 유한한 규칙으로 무한한 구조를 정의하는 방법Syntax vs Semantics
→ 프로그램의 형태와 의미를 구분하는 방법Inference Rules
→ 규칙을 통해 프로그램과 의미를 형식적으로 정의하는 방법
이 세 가지는 이후 등장할 모든 개념의 기반이 된다.
조금 더 큰 그림에서 보면, 지금까지 한 일은 이것이다.
\[\text{“프로그램을 어떻게 정의할 것인가”}\]하지만 아직 중요한 질문이 남아 있다.
“그렇게 정의된 프로그램의 성질은 어떻게 증명할까?”
또는 더 직접적으로 말하면,
“이 프로그램이 항상 올바르게 동작한다는 것을 어떻게 보장할까?”
다음 글에서는 이 질문에 답하기 위해
Structural Induction (구조적 귀납법) 을 살펴본다.
이 개념은 단순한 증명 기법이 아니라,
프로그래밍 언어 이론 전체를 지탱하는 핵심 도구
이기 때문에 반드시 제대로 이해해야 한다.