🔁 다시 보기: 문제의 문장

<while b do S1, s''> → s' 가 주어졌을 때,

<while b do S1, s''> ⇒* s' 를 증명하기 위해 귀납 가정을 쓸 수 있는가?

이 상황은 <while b do S1, s> → s'를 증명 중에, <while b do S1, s''> → s'라는 하위 도출이 등장하는 경우야.

🧮 수식적 정리: 두 귀납법의 차이

✅ Structural Induction (on S)

• 귀납 대상: S ∈ Stmt (구문구조)
• 목표: ∀S. P(S)
• 귀납 구성:
  • Base cases: S = skip, x := a
  • Inductive cases: 예를 들어 S = while b do S1이면,P(S1)을 가정하여 P(S)를 증명해야 함
• 필요 조건: S1이 S보다 구조적으로 "작다" (서브트리 구조)

❌ 실패 이유:

• while은 다음과 같은 big-step 규칙을 가짐:

  beval(b, s) = true
  <S1, s> → s1      <while b do S1, s1> → s2
  ————————————————————————————————————————————————
  <while b do S1, s> → s2
  

• 두 번째 전제 <while b do S1, s1> → s2 는 S와 구조적으로 동일

  → Structural induction 적용 불가 (순환 구조가 작아지지 않음)

✅ Induction on the Derivation (on <S, s> → s')

• 귀납 대상: 도출 트리 D such that D ⊢ <S, s> → s'
• 목표: ∀도출 D. P(D)
• 귀납 구성:
  • Base cases: 도출 깊이가 1인 경우 (e.g., skip, assign, while-false)
  • Inductive step: D의 premise 도출들이 모두 성립한다고 가정하고 D 전체에 대해 증명

✅ 가능한 이유:

• 도출 <while b do S1, s> → s'는 다음을 포함함:

  D1: <S1, s> → s1      D2: <while b do S1, s1> → s2
  ————————————————————————————————————————————————
  D:  <while b do S1, s> → s2