Butterfly라는 프로그래밍 언어를 만들고 있는 중에 문제가 발생해서 여쭙니다.

일단, 이 논리형 언어를 소개할게요. 논리형 언어이지만 한정사(quantifier)나 결합자(connective)는 없습니다.

먼저 기본적인 객체로는 생성자(constructor), 변수(variable), 술어(Predicate), 형(Type)이 있습니다.

값: n항 생성자가 n개의 값과 결합한 것이며 한 값은 한 타입에만 속합니다.

항: 변수 그 자체이거나 n항 생성자가 n개의 항들과 결합한 것입니다.

명제: n항 술어가 n개의 값과 결합한 것입니다.

식: n항 술어가 n개의 항과 결합한 것입니다.

공리: 0개 이상의 식들을 전제들로, 1개의 식을 결론으로 가집니다.

예를 들어 타입 Nat을 다음과 같이 정의합시다.

Nat ::= zero( ), succ( Nat ).

그러면 zero( ), succ( zero( ) ), succ( succ( zero( ) ) ), ... 등은 모두 Nat에 속하는 서로 다른 값들입니다.

그리고 1항 술어 Even에 대하여 Even( x )와 Even( succ( succ( x ) ) )은 적법한 식입니다.

원래 타입이 맞아야 적법한 항이 되고 식이 되지만 여기서는 타입이 항상 맞다고 가정하겠습니다.

변수배정은 한 식에 있는 모든 변수를 값으로 치환하여 그 식을 명제로 바꾸는 행위입니다.

명제 A에 대하여 적당한 공리와 그 공리에 대한 변수배정이 존재하여

변수배정된 공리의 결론이 A와 같고 변수 배정된 전제들이 모두 증명가능하면 A는 증명가능합니다.

Butterfly 인터프리터는 사용자가 코딩한 공리들을 해석하여 사용자가 질의한 명제가 증명가능한지 알려줍니다.

예를 들어 다음과 같이 코딩했다고 합시다. (공리는 '전제1, ..., 전제n / 결론' 꼴로 코딩됩니다.)

  1. / Even( zero( ) ).

  2. Even( x ) / Even( succ( succ( x ) ) ).

이때 "Even( succ( succ( zero( ) ) ) )?"라고 물으면 "yes"라고 답하고
"Even( succ( zero( ) ) )?"라고 물으면 "no"라고 답합니다.

그런데 자유 변수들을 정의하면 그것들이 있는 식이 증명가능한지 알려줄 수 있습니다.

예를 들어 자유변수 a와 b를 다음과 같이 정의할 수 있습니다.

  • a : Nat.

  • b : Nat.

  • a → zero( ), succ( b ).

  • b → succ( a ).

첫 번째 줄과 두 번째 줄은 각각 a와 b가 타입 Nat에 속한다는 것을 의미합니다.
세 번째 줄과 네 번째 줄은 이렇게 해석할 수 있습니다:
a가 가질 수 있는 값의 집합은 zero( )를 원소로 가지며 임의의 b에 대하여 succ( b )를 원소로 가진다,
b가 가질 수 있는 값의 집합은 임의의 a에 대하여 succ( a )를 원소로 가진다.
이때 "Even( a )?"라고 물으면 a에게 정의에 따르는 임의의 값이 배정될 때 식 Even( a )이 항상 증명가능한지를 답합니다.
a가 가질 수 있는 값은 zero( ), succ( succ( zero( ) ) ), ... 뿐이므로 "yes"라고 답하겠지요.
드디어 문제를 말할 수 있게 됐네요. Even( a )를 어떤 논리식으로 바꿔야 합니까?

제 생각에는 귀납법을 변형해야할 것 같습니다.

제 생각에는 Even( a )가 증명가능할 때 그리고 그럴 때에만 다음 두 논리식 모두 참일 것 같습니다.

  • ∀a [ Even( a ) → Even( zero( ) ) ].
  • ∀a [ Even( a ) → ∀b [ Even( b ) → Even( succ( succ( a ) ) ) ] ].
첫 번째 논리식은 a → zero( )에서 바로 얻어지며,
a → succ( b )에서 ∀a [ Even( a ) → Even( succ( b ) ) ]를 얻고
다시 b → succ( a )에서 두 번째 논리식이 얻어집니다.

이게 맞나요? 즉, 자유변수 x : T와 항 t : T에 대하여

변수 정의 x → t에서 논리식 ∀x [ φ → φ[x := t] ]를 얻을 수 있나요?

제 생각에는 이게 귀납법과 비슷해서 제목을 그렇게 썼습니다.

아무튼 긴 글 읽어주셔서 감사하고 고민해 주시면 더욱 감사하겠습니다.

그리고 이것의 구현까지 고민해주시면 더더욱 감사하겠습니다.