Inference Rules (추론 규칙)

추론 규칙은 프로그래밍 언어나 수학에서 특정 조건이 충족되었을 때, 어떤 결론을 내릴 수 있는지에 대한 논리적인 규칙이다.

특히 Operational Semantics에서 이러한 규칙은 프로그램의 동작을 수학적으로 설명하는 데 사용된다.

 

추론 규칙은 크게 두 부분으로 나눌 수 있다.

 

추론 규칙 예시 : 

 

H1   H2   ...   Hn
-----------------
       C

 

1. 전제 (Hypotheses)

프로그램의 특정 조건을 나타낸다. 여기서 H1, H2처럼 표현되는 부분들이 전제다. 여러 전제가 있을 수 있고, 이들이 참일 때 결론을 도출할 수 있다.

2. 결론 (Conclusion)

전제들이 참이면, 그에 따라 도출되는 결론이다. C로 표시되며, 전제들로부터 유추할 수 있는 결과를 말한다.

 

이 구조 예시에서, H1, H2, ..., Hn은 여러 전제이고, 이 전제들이 모두 만족되면 C라는 결론이 도출된다.

이를 논리적으로 표현하면 다음과 같다.

H1 ∧ H2 ∧ ... ∧ Hn ⇒ C

즉, 전제가 모두 참일 경우 결론 C도 참이라는 거다.

비유를 들자면 

냉장고에 피자가 있는 걸 알고 있고(H₁), 그 피자는 내 것이라는 것도 알고 있고(H₂) 그리고 냉장고가 고장 나지 않았다는 것도 알고 있다(Hₙ)

그러면, "그래, 피자를 먹을 수 있겠다!"(C)라고 결론을 내릴 수 있는 것이다.

 

다음은 또 다른 예시다.

e1 ⇒ n1   e2 ⇒ n2
-------------------------------
  e1 + e2 ⇒ n1 + n2

 

이 규칙은 e1이 n1으로 계산되고, e2가 n2로 계산될 때, e1 + e2는 n1 + n2로 계산된다는 의미다.

 

이제 증명 예시를 살펴보자.

만약 다음과 같은 식을 증명해야한다고 가정해보자.

4 + (2 - 1) ∈ A

즉, 4라는 숫자랑 2 - 1을 더한 결과가 A라는 집합에 속하는지 증명해야 한다.

여기서 사용되는 규칙을 알아보자

n ∈ ℤ ⇒ n ∈ A: 정수는 A에 속할 수 있다는 규칙

e₁ ∈ A ∧ e₂ ∈ A ⇒ e₁ + e₂ ∈ A: 두 표현식이 A에 있으면 더해도 A에 속한다는 규칙

e₁ ∈ A ∧ e₂ ∈ A ⇒ e₁ - e₂ ∈ A: 두 표현식이 A에 있으면 빼도 A에 속한다는 규칙

 

이제 증명 세부 과정을 살펴보자

 

• 4 ∈ ℤ이니까, 4 ∈ A (정수 4가 A에 속함).
• 2 ∈ ℤ이니까, 2 ∈ A (정수 2도 A에 속함).
• 1 ∈ ℤ이니까, 1 ∈ A (정수 1도 A에 속함).

이제 2 - 1이 A에 속하는지 봐야한다.

2 ∈ A이고 1 ∈ A니까, 빼도 A에 속해. 즉, 2 - 1 ∈ A가 된다.

 

마지막으로 4 + (2 - 1) ∈ A 만 증명하면 된다.

4 ∈ A이고 2 - 1 ∈ A니까, 더해도 A에 속한다.

그래서 4 + (2 - 1) ∈ A를 증명할 수 있었다.

 

---

다음은 새로운 표현에 대해 알아보자

 

만약 이런 식이 있다고 해보자

⊆ A × ℤ

⊆는 부분집합을 의미하는데 즉, A × ℤ라는 건 A와 ℤ의 카르테시안 곱을 말하는 거다.

그냥 A는 ℤ와 관련된 값들을 가지고 있다고 생각하면 된다.

 

그리고 다음 식을 살펴보자

⊢ 4 + (2 - 1) ⇒ 5

⊢는 논리적으로 "증명할 수 있다"라는 뜻이다.

즉, 4 + (2 - 1) ⇒ 5라는 건, "4와 2에서 1을 빼서 더하면 5가 된다"라는 사실을 증명할 수 있다는 의미다.