안녕하세요, 수잘갤러 여러분. 기말고사는 잘 보셨습니까?

아시는 분은 아시겠지만 저는 저만의 프로그래밍 언어를 개발 중인데요,

논리형 언어인 Prolog를 개량하여 Butterfly 언어를 만들고자 합니다.

자세한 설명은 여기에 있습니다:

http://gall.dcinside.com/mgallery/board/view/?id=github&no=760&search_head=30&page=1

즉, 한정사 없는 원자논리식 α_1, ..., α_n, β, φ과 변수들의 열 x에 대하여,

∀x (α_1 ∧ ... ∧ α_n → β) 꼴의 공리를 코딩하고 인터프리터에게 φ를 질의하면,

인터프리터는 코딩된 공리계 상에서 Φ가 언제 참인지를 답합니다.

다음 코드를 봅시다:

1 Nat -- 타입 Nat 정의.

2 {

3 zero( ) → "z". -- 0항 생성자 zero 정의.

4 succ( Nat ) → "s" 1. -- 1항 생성자 succ 정의.

5 }

6 Main( Nat ). -- 1항 술어 Main 선언.

7 / Main( zero( ) ). -- 식 Main( zero( ) )는 항상 참이다.

8 Main( n ) / Main( succ( n ) ). -- 식 Main( n )이 참일 때, 식 Main( succ( n ) )이 참이다.

수학적 귀납법에 의하여 임의의 n : Nat에 대하여 식 Main( n )은 항상 참이어야 합니다.

그러므로 다음은 위의 코드 상에서 가능한 질의와 응답입니다.

≪ Main( n )? -- 질의: 변수 n에 어떤 값이 배정될 때 식 Main( n )은 참인가?

≫ n : Nat. -- 응답: n의 타입이 Nat이기만 하면 된다.

모든 변수배정을 열거하게끔 인터프리터를 설계해도 되겠지만

그러면 모든 n을 나열할 수 없을 뿐만 아니라 큰 의미가 없는 구현이 되겠지요.

문제는 귀납법을 구현하기는 커녕 귀납법을 정의하는 것 조차 힘들다는 것입니다.

structural induction을 mutually recursive datatypes에 대해서도 적용할 수 있게끔 정의해야돼요.

그리고 인터프리터가 언제 귀납법을 적용할지 전략을 짜는 것도 힘듭니다.

그래서 이 두 가지를 여러분께 질문합니다.