저는 기계공학도이지만 프로그래밍 언어를 만드는 게 꿈이고 그 인터프리터에 증명보조기 기능을 추가하고 싶습니다. 증명보조기가 Coq처럼 대단한 게 아니라, inference rule들을 읽고 judgment들이 올바르게 유도되었는지 확인하는 게 다입니다. 즉, 다른 증명보조기들과 다르게 사용자가 inference rule들을 입력해야 합니다. 저는 논리학 지식이 없어서 inference rule들의 완전성을 판별할 수 없으므로 증명보조기를 사용할 때 inference rule를 입력하도록 한 것입니다. 좋은 아이디어가 있다면 알려주세요. 일단, 제 아이디어를 소개할게요.
#fn and(bool, bool) : bool.
#ir and_intro(bool, bool) : bool
{
___ (Hyps |- A::true), (Hyps |- B::true) → (Hyps |- and(A, B)::true)
}
먼저 함수 and의 자료형을 선언해준 뒤, 추론 규칙을 코딩했습니다.
람다 추상화로 변수의 묶임을 표현하고자 합니다.
항 M : tau에 대하여 $x:sigma → M은 tau[sigma]형의 항입니다.
따라서 함수 for_all를 다음과 같이 선언할 수 있습니다.
#fn for_all(bool[t]) : bool.
그런데 추론 규칙을 코딩하는 데 문제가 있습니다.
#ir for_all_intro(bool) : bool
{
___ (Hyps |- A::true) → (Hyps |- for_all($x:t → A)::true)
___ ___ $x:t ~ Hyps
}
$x:t ~ Hyps는 변수 $x가 항들의 집합 Hyps의 자유변수가 아니라는 뜻인데, $x:t의 identity를 어떻게 알 수 있을까요?
참고로 소거 규칙은 다음과 같이 코딩할 수 있습니다.
#ir for_all_elim(bool, t) : bool
{
___ (Hyps |- for_all($x:t → A)::true), (Hyps |- T::exist) → (Hyps |- A[$x:=T]::true)
}
항 A[$x:=T]는 항 A 안의 변수 $x의 모든 자유나타남이 항 T로 치환되어 얻어진 것입니다.