문법과 의미론 (Grammar & Semantics)

1. Overview

문법과 의미론(Grammar & Semantics)은 프로그래밍 언어가 "어떤 코드가 문법적으로 올바른가(Syntax)"를 넘어, "그 코드가 실행될 때 어떤 의미인가(Semantics)"를 수학적으로 정의하는 형식 언어 이론(Formal Language Theory)의 기초 공학입니다.

학습자는 정규 문법(Regular Grammar)→문맥 자유 문법(Context-Free Grammar, CFG)→문맥 의존 문법(Context-Sensitive Grammar)의 촘스키 계층(Chomsky Hierarchy)을 살펴봅니다. 나아가 CFG의 BNF/EBNF 표기와 파스 트리(Parse Tree), 추상 구문 트리(AST)를 거쳐 연산 의미론(Operational Semantics), 표시 의미론(Denotational Semantics), **공리 의미론(Axiomatic Semantics, Hoare Logic)**의 세 가지 프로그램 의미 정의 방식을 비교하고, 프로그래밍 언어 설계와 검증(Program Verification)의 이론적 토대를 확보합니다.

2. Scope & Boundaries

In-Scope

• 촘스키 계층 (Chomsky Hierarchy): 정규 언어(Regular, Type 3), 문맥 자유 언어(CFL, Type 2), 문맥 의존(Type 1), 재귀 열거(Type 0)의 포함 관계와 인식 기계.
• 문맥 자유 문법 (CFG): BNF/EBNF 표기법, 유도(Derivation), 파스 트리(Parse Tree), 모호성(Ambiguity), CNF(촘스키 정규 형태).
• 추상 구문 트리 (AST): 파스 트리 → AST 변환, AST 노드 설계, 방문자 패턴(Visitor Pattern).
• 프로그램 의미론 (Semantics): 연산 의미론(Small-step/Big-step), Hoare Logic(사전/사후 조건), 타입 건전성(Type Soundness, Progress & Preservation).

Out-of-Scope

• 렉서/파서 구현 도구: Lex/Yacc, ANTLR 도구 사용법 → 05-02-01. Frontend Compilers 영역.
• 정리 증명기(Proof Assistant): Coq, Isabelle 같은 형식 검증 도구 → Formal Verification 영역.

Boundaries

• 문법(Syntax) vs 의미(Semantics): 문법은 "어떤 토큰 열이 유효한 문장인가"를 정의(파서가 처리). 의미론은 "유효한 문장이 실행되면 무슨 일이 일어나는가"를 정의(인터프리터/컴파일러가 처리). x + y * z는 문법적으로 올바르지만, *가 +보다 우선순위가 높다는 것은 의미론(Semantic)의 영역입니다.

3. Counterexample

• 모호한 문법과 파스 트리의 충돌 (Ambiguous Grammar): 문법 E → E + E | E * E | (E) | id로 a + b * c를 파싱하면, (a+b)*c로도, a+(b*c)로도 파싱 가능한 두 개의 파스 트리가 생성됩니다. 이런 모호한 문법(Ambiguous Grammar)은 파서가 어떤 규칙을 먼저 적용해야 할지 결정할 수 없어 언어가 의도한 의미를 잘못 계산할 수 있습니다. 우선순위(Precedence)와 결합성(Associativity)을 문법 규칙 자체에 인코딩하여 비모호 문법(Unambiguous Grammar)을 만들어야 합니다.
• 타입 건전성 위반과 런타임 타입 오류 (Type Unsoundness): 동적 타입 언어(Python, JavaScript)에서 def add(x, y): return x + y를 add("hello", 42) 로 호출하면 문법적으로는 허용되지만, 런타임에 TypeError: can only concatenate str (not "int") to str가 발생합니다. 정적 타입 시스템(Haskell, Rust)은 이 오류를 컴파일 시점에 타입 추론으로 탐지하여 런타임 타입 오류 가능성을 줄입니다.

4. Prerequisites

• 오토마톤 기초 (Basic): 정규 문법을 인식하는 유한 오토마톤(DFA/NFA) 개념이 필요합니다. (04-04-02 String Matching & Automata)
• 재귀 (Basic): CFG 유도와 파스 트리 구축이 재귀 기반입니다. (04-03-01 Recursion)

5. Learning Map

6. Learning Topics

Basic

Core Topic 01: 언어 클래스의 계층과 정규의 한계, 촘스키 계층 (Chomsky Hierarchy)

• Why to Learn: 정규 표현식(RegEx)이 HTML 파싱에 적합하지 않은 이유(HTML은 정규 언어가 아닌 CFL), XML/JSON 파서가 스택 기계를 요구하는 이유의 형식 언어 이론적 근거를 이해하기 위해서입니다.
• What to Learn:
  • Concepts: 촘스키 계층(Type 0~3), 정규 언어(DFA 인식), 문맥 자유 언어(PDA 인식), 펌핑 보조 정리(Pumping Lemma).
  • Skills: 펌핑 보조 정리로 특정 언어가 정규가 아님을 증명.
• How to Learn:
  • 1단계: a^n b^n (같은 수의 a와 b) 언어가 정규가 아님을 펌핑 보조 정리로 증명합니다. DFA는 유한 상태(Finite State)라 n의 정확한 카운트를 기억할 수 없어 무한한 {ab, aabb, aaabbb,...}를 인식할 수 없음을 확인합니다.
  • 2단계: HTML의 중첩 태그 <a><b></b></a>는 a^n b^n 패턴(여는 태그 = a, 닫는 태그 = b)과 동일 구조라 정규 언어로 파싱하기 어렵습니다. CFG로는 가능한 이유를 살펴봅니다.
• Implement: 파이썬 SimpleLanguageChecker. 정규 표현식으로 a^n b^n 언어를 파싱 불가임을 re.match(r'^a+b+$', 'aaabbb') 가 단순 패턴만 확인하고 n=n 균형을 검증 못함을 증명. 반면 재귀 함수로 check_balanced(s) → O(n) 균형 확인 가능 비교.

Recommended

Core Topic 02: BNF로 언어를 정의하고 트리로 읽다, CFG와 파스 트리 (CFG & Parse Tree)

• Why to Learn: 프로그래밍 언어 설계자가 새 언어의 문법을 BNF로 규정하고, 컴파일러 프론트엔드가 소스 코드를 파스 트리로 변환하는 과정이 모든 컴파일러의 출발점임을 이해하기 위해서입니다.
• What to Learn:
  • Concepts: BNF(Backus-Naur Form), EBNF, 생산 규칙(Production Rule), 유도(Derivation), 최좌측/최우측 유도(Leftmost/Rightmost Derivation), 파스 트리(Parse Tree) vs AST.
  • Skills: 주어진 문법에서 특정 문자열 유도하기, 모호성 제거(Precedence/Associativity 규칙 인코딩).
• How to Learn:
  • 1단계: 산술식 BNF: E → E + T | T; T → T * F | F; F → (E) | num. 이 문법은 *가 +보다 우선순위 높음을 구조적으로 인코딩합니다. 2+3*4의 파스 트리에서 3*4가 먼저 계산되는 트리 구조를 분석합니다.
  • 2단계: 파스 트리 → AST 변환. 파스 트리는 문법 규칙을 그대로 반영(중간 E, T, F 노드 포함)하지만 AST는 의미에 필요한 노드만 추출(+ 노드, 자식 2와 * 노드, *의 자식 3, 4)하여 단순화하는 과정을 살펴봅니다.
• Implement: 파이썬 재귀 하강 파서(Recursive Descent Parser). parse_expr(), parse_term(), parse_factor() 함수로 산술식 문자열을 파싱하여 AST(딕셔너리 트리) 구축. "2+3*4" → {op:'+', left:2, right:{op:'*', left:3, right:4}} AST 출력 + 재귀 eval로 14 계산 검증.

Practical

Core Topic 03: 한 스텝씩 실행의 수학, 연산 의미론 (Operational Semantics)

• Why to Learn: 프로그래밍 언어 설계자가 "이 언어에서 while 루프가 정확히 어떻게 실행되는가"를 자연어 설명이 아니라 수학적 추론 규칙으로 명세(Specification)하는 방법을 이해하고, 인터프리터 구현의 정확성을 높이기 위해서입니다.
• What to Learn:
  • Concepts: Small-step SOS(Structural Operational Semantics, 한 스텝 실행), Big-step(Natural Semantics, 전체 실행 결과), 구성(Configuration ⟨S, σ⟩), 전이 관계(→).
  • Skills: if-then-else, while 루프의 추론 규칙 읽기/쓰기.
• How to Learn:
  • 1단계: Small-step SOS while 규칙: ⟨while b do S, σ⟩ → ⟨if b then (S; while b do S) else skip, σ⟩. 단 한 스텝에서 while을 if문으로 풀어냅니다. 이 규칙을 반복 적용하여 while의 실행을 시뮬레이션하는 방식을 분석합니다.
  • 2단계: Big-step(Natural) 의미론: ⟨S, σ⟩ ⇓ σ' (명령 S가 상태 σ에서 실행되어 최종 상태 σ'을 만든다). 대입문 규칙 ⟨x:=a, σ⟩ ⇓ σ[x↦⟦a⟧σ]를 읽는 방법을 익힙니다.
• Implement: 파이썬 간단 인터프리터(Toy Language). Expr: Num | Add | Mul | Var. Stmt: Assign | Seq | IfElse | While. eval_expr(expr, env) + exec_stmt(stmt, env) 구현. x=1; while x<10: x=x*2 → env={'x':16} 실행 후 상태 검증. 각 스텝 출력으로 Small-step SOS 시뮬레이션.

Advanced

Core Topic 04: 수학으로 코드를 증명하다, Hoare Logic (Hoare Triple & Program Verification)

• Why to Learn: NASA 우주선 소프트웨어, 의료 기기 펌웨어, 금융 핵심 계산 모듈처럼 높은 신뢰성이 필요한 코드에서 프로그램 검증(Program Verification)의 이론적 기반으로 Hoare Logic이 어떻게 쓰이는지 이해하기 위해서입니다.
• What to Learn:
  • Concepts: Hoare Triple {P} C {Q} (P: 사전 조건, C: 명령, Q: 사후 조건), 대입 공리, 순차 합성 규칙, while 루프 불변식(Loop Invariant).
  • Skills: 루프 불변식 도출, 약화(Weakening)/강화(Strengthening) 규칙.
  • Tools: Frama-C(C 코드 검증), Dafny, Z3 SMT Solver.
• How to Learn:
  • 1단계: {x=n} x:=x+1 {x=n+1} Hoare Triple 검증. 대입 공리: {Q[x←a]} x:=a {Q} 를 역방향으로 Q={x=n+1}, Q[x←x+1]={x+1=n+1} = {x=n}. 사전 조건이 정확히 {x=n}이므로 Triple이 성립하는 과정을 확인합니다.
  • 2단계: 루프 불변식(Loop Invariant)으로 while 증명. sum = 0; i = 0; while i < n: sum += i; i += 1. 불변식 I: sum = i*(i-1)/2. 진입 전 I 성립 검증, 루프 본체 후 I 유지 검증, 종료 후 I ∧ ¬(i<n) → sum = n*(n-1)/2 최종 결론 도출을 살펴봅니다.
• Implement: 파이썬 verify_hoare_triple(pre, stmt, post, test_cases). 사전 조건, 명령(람다 함수), 사후 조건을 받아 test_cases 값들에서 사전→실행→사후 검증 자동화. {x>0} x:=x*2 {x>0} 100개 랜덤 테스트로 소프트웨어 테스트 기반 검증 모사.

7. Terminology

8. References

Primary

• [P1] CS2023 - Programming Languages (PL) - Syntax and Semantics
• [P5] SFIA - Software Design (SWDN) - Language Formalism

Secondary

• [Types and Programming Languages] Benjamin C. Pierce - Operational Semantics and Formalization
• [Programming Language Pragmatics] Michael L. Scott - Scope, Binding, and Evaluation

Industry

• [ECMAScript Language Specification] - Lexical Environment and Scope Rules
• [Python Language Reference] - Execution Model and Naming

9. Final Checklist

Primary

• 정규 표현식(Regular Expression)으로 변수명을 식별하고, 문맥 자유 문법(CFG)으로 if-else 블록의 중첩 구조를 해석하는 차이를 설명할 수 있는가?
• 구문 에러(Syntax Error)와 런타임 의미 에러(Semantic Error)의 발생 시점과 원인을 명확히 구분할 수 있는가?

Secondary

• 렉시컬 스코프(Lexical Scope)를 사용하는 언어에서 클로저(Closure)가 형성될 때, 자유 변수(Free Variable)가 메모리에 바인딩되는 메커니즘을 설명할 수 있는가?
• 소스 코드가 Abstract Syntax Tree (AST)로 변환되는 과정을 묘사하고, 이것이 인터프리터 패턴(Interpreter Pattern)에서 어떻게 순회(Traversal)되는지 설명할 수 있는가?

Industry

• 특정 언어의 조작적 의미론(Operational Semantics) 명세가 실제 가상 머신(VM)의 레지스터나 스택 상태 변화로 어떻게 매핑되는지 아키텍처 관점에서 논증할 수 있는가?
• 프로그래밍 언어의 평가 전략(Call-by-value vs Call-by-reference/Call-by-need) 차이가 대규모 객체 전달 시 발생하는 메모리/CPU 부하에 미치는 영향을 설계할 수 있는가?