viewimage.php?id=2ab4c42ef0d0&no=24b0d769e1d32ca73fee85fa11d02831d7eb5c9acd2fe50a30ee0df9037efe433928504c78bc46cfc7fe4f55286317e76405f24abf40d1cd85a024dc875c0a1e48

1. butterfly

butterfly는 함수형 언어임.

물론 butterfly 인터프리터를 증명보조기로서 쓸 수 있도록 개발할 거임.

함수형 언어로서 butterfly를 소개할게.


2. 구조체

예약어를 적고, 이름을 적고, 타입 파라메터를 선언한 다음,

상속 받을 구조체 이름을 적고,

타입들을 정의하고 함수들을 선언하면

구조체 정의가 완료됨.

예를 들어 구조체 pl을 정의할 때

bool이란 타입을 정의했고

6개의 함수들을 선언했음.

그리고 구조체 fol을 정의할 때

타입 파라메터 T를 선언하고

pl을 상속 받은 다음

3개의 함수들을 선언했음.


3. 시스템

예약어를 적고, 이름을 적고,

불러올 시스템 이름을 적고,

타입들을 정의하고 함수들을 정의하고,

구조체의 인스턴스를 정의하면

시스템 정의가 완료됨.

시스템 main을 정의할 때

nat이란 타입을 정의했고

함수 plus를 정의한 다음

fol_nat이라는 이름을 가진

구조체 fol＜nat＞의 인스턴스를 정의했어.


4. 바인더

butterfly 인터프리터는 지시파일을 읽고 사용자와 대화할 수 있어.

사용자와 대화할 때 (∀x∈N)( x = 0 ) 같은 질문에도 답하는 게 목표야.

∀, ∃의 의미는 다들 잘 알지?

그런데 얘들은 변수를 묶잖아.

그래서 바인더 []를 도입했어.

위 질문을 butterfly식으로 바꾸면 for_all[X:nat](equal(X, zero()))야.

이게 계산될 때 변수 X는 $x에 매칭되고 항 equal(X, zero())는 A에 매칭돼.

항 A 안의 변수 $x의 자유 나타남이 항 N으로 모두 바뀌어 버린 것을 A[$x:=N]라 표기해.

규칙 A ⇒ check(zero())과 규칙 N ⇒ and(A[$x:=N], check(succ(N))에 의해

equal(X, zero())는 and(equal(zero(), zero()), check(succ(zero())))가 되고

check(succ(zero()))가 and(equal(succ(zero()), zero()), check(succ(succ(zero()))))가 되므로

for_all[X:nat](equal(X, zero()))은 false()로 평가되지.


이상으로 함수형 언어로서 butterfly를 소개를 마치고,

다음 번에는 판정규칙을 작성하는 법에 대해 설명할게.

질문 환영, 댓글 환영.