1. Compositional semantics

• 형식: 의미 함수 ⟦·⟧ : Syntax → Domain을 정의.
• 방법: 복합 구문은 하위 구문의 의미를 수학적 함수 조합으로 표현.
  • 예: ⟦e1 + e2⟧ρ = ⟦e1⟧ρ + ⟦e2⟧ρ
• 의도: Frege의 합성 원리(Frege’s Principle of Compositionality)를 따름.
  • 의미는 항상 “부분 의미”와 “구문 구조”만으로 정해진다.
• 결과: 함수 정의라서, 프로그램 의미는 곧바로 하나의 수학적 객체(숫자, 상태 변환 함수, 집합 등).

2. Inductive semantics

• 형식: inference rules (추론 규칙)로 프로그램 의미를 귀납적으로 정의.

• 방법: “이전 구문이 어떤 의미를 가진다”를 전제로 두고, “전체 구문은 이런 의미를 가진다”는 규칙을 세움.

  • 예 (big-step):

    ⟨e1, σ⟩ ⇓ n1    ⟨e2, σ⟩ ⇓ n2
    ------------------------------
        ⟨e1+e2, σ⟩ ⇓ n1+n2
    

• 의도: 프로그램 실행이나 평가 과정을 “증명 절차(proof tree)”로 표현.

• 결과: 프로그램의 의미는 “이 구문이 이렇게 평가된다”는 도출 과정 전체.

3. 차이 요약

• compositional: 의미를 함수적으로 조합 → 정의 자체가 수학적 함수/식.
• inductive: 의미를 규칙적으로 도출 → 정의 자체가 inference system.
• compositional은 “함수적 계산”, inductive는 **“논리적 추론”**이라고 생각하면 됩니다.
• 특히 while 같은 반복문에서 차이가 확실히 드러나요:
  • compositional: 고정점 연산자(fixpoint)로 정의.
  • inductive: 반복 실행 규칙을 귀납적으로 계속 적용.

👉 즉, 두 방식 다 “부분 의미를 결합한다”는 점에서 닮았지만,

• compositional은 정의가 함수적이고,