설명서를 유동이 원해서 쓰긴 하는데 사실 언젠가는 써야했던 것이긴 합니다.

설명이 ㅄ같아도 이해해주세요.


0. 개요: 구문론, 코드 작성, 의미론, 질의와 응답.


1. 구문론

Butterfly에서 기본 객체는 타입, 술어, 변수, 생성자의 4가지 종류 중 하나입니다.

다른 객체는 무엇이고 어떻게 만드는지 알아봅시다.


1.1 값

값은 n항 생성자가 n개의 값과 결합한 것입니다.

즉, 0항 생성자는 그 자체로 값입니다.


1.2. 항

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

즉, 모든 값은 항입니다.


1.3. 식

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


1.4. 타입

모든 결합이 적법한 것은 아닙니다. 타입이 일치해야 합니다.


1.5. 공리

0개 이상의 식을 전제로 하고 1개의 식을 결론으로 합니다.


2. 코드 작성

Butterfly에서 모든 문장은 타입선언, 타입 정의, 술어 선언, 공리 생성 4 가지 중 하나입니다.


2.1. 식별자(identifier)

타입, 술어, 변수, 생성자만이 식별자를 가집니다.

타입과 술어의 식별자는 대문자 또는 소문자의 유한열이며 첫 글자는 무조건 대문자입니다.

변수와 생성자의 식별자는 소문자 또는 숫자 또는 밑줄문자의 유한열이며 첫 글자는 무조건 소문자입니다.

예를 들어 Nat은 타입의 식별자가 될 수 있고 n_1은 변수의 식별자가 될 수 있습니다.


2.2. 타입 선언

타입의 식별자가 될 수 있는 문자열에 점을 붙이면 됩니다.

Nat이라는 타입을 선언하고 싶으면 다음과 같이 하면 됩니다.

  1. Nat.


2.3. 술어 선언

술어의 식별자가 될 수 있는 문자열 뒤에 괄호와 점을 붙이고

괄호 안에 각 항이 취할 타입을 적어주면 됩니다.

예를 들어 자연수를 첫 번째 항으로 취하는 1항 술어 Main을 다음과 같이 선언할 수 있습니다.

  1. Main( Nat ).


2.4. 타입 정의


타입의 식별자를 쓴 다음 중괄호를 붙이고

중괄호 안에서 생성자들을 정의합니다.

생성자들은 그것의 각 항이 취하는 타입과 형식문법의 생성규칙에 의하여 정의됩니다.

예를 들어 타입 Nat을 다음 코드에서처럼 0항 생성자 zero와 1항 생성자 succ으로 정의할 수 있습니다.

  1. Nat
  2. {
  3.     zero( ) → 'z'.
  4.     succ( Nat ) → 's' 1.
  5. }

여기서 0항 생성자 zero( )와 대응되는 문자열은 'z'이고,

첫 번째 항의 타입으로 Nat을 가지는 1항 생성자 succ( Nat )과 대응되는 문자열은 's' 1입니다.

단, 이때 1은 succ의 첫 번째 항과 대응되는 문자열을 의미합니다.


2.5. 공리 생성

전제가 되는 식들을 쓰고 "/"를 붙인 뒤 결론을 쓰고 점을 붙입니다.

예를 들어 다음과 같이 공리 2개를 코딩할 수 있습니다.

  1. / Main( zero( ) ).
  2. Main( n ) / Main( succ( n ) ).


3. 의미론

이제 작성한 코드가 무슨 의미인지 알아봅시다.


3.1. 값

생성자가 값들과 결합한 것이 값이라고 말했죠?

그러므로 succ( zero( ) )나 succ( succ( zero( ) ) )은 값입니다.

모든 적법한 값은 타입에 속하고 문자열로 변환될 수 있습니다.

위의 두 값은 Nat에 속하고 각각 'sz'와 'ssz'로 변환될 수 있습니다.

succ과 대응되는 문자열은 's' 1이고 zero와 대응되는 문자열은 'z'이므로

succ( zero( ) ) → 's' zero( ) → 's' 'z' ???? 'sz'이고

succ( succ( zero( ) ) ) → 's' succ( zero( ) ) → 's' 's' zero( ) → 's' 's' 'z' ???? 'ssz'이기 때문입니다.

한편 위의 두 값이 서로 다름을 알 수 있습니다.


3.2. 항

변수 그 자체로 항이 될 수 있고, 생성자가 항들과 결합해도 항입니다.

그러므로 succ( n ), succ( succ( n ) )은 항입니다.

모든 적법한 항은 타입에 속하고 위의 두 항은 Nat에 속합니다.

여기서 위 두 항은 각각 's' n과 'ss' n으로 변환될 수 있습니다.

한편, 항에 있는 모든 변수들에 값을 배정하여 그 항을 값으로 평가할 수 있습니다.


3.3. 식

술어가 항들과 결합한 것으로 Main( succ( n ) )이나 Main( 's' n )은 식입니다.

항 succ( n )을 문자열로 변환하면 's' n이기 때문에

인터프리터는 위 두 식을 같다고 간주합니다.

식에 있는 모든 변수에 변수 배정에 따라 값을 배정하면

식이 유도될 수 있는지 없는지를 논할 수 있습니다.


3.4. 공리

각 공리는 임의의 변수 배정에 대하여 전제들이 모두 유도될 수 있을 때 결론도 유도될 수 있다는 뜻을 가집니다.

"/ Main( zero( ) )." 같은 공리는 전제들의 집합이 공집합이므로 식 Main( 'z' )는 임의의 변수 배정에 대하여 항상 유도될 수 있습니다.

그리고 공리 "Main( n ) / Main( succ( n ) )."에 의하여 식 Main( 'sz' )가 유도되고 다시 식 Main( 'ssz' )가 유도되고 ....

한편, 공리를 생성자와 괄호를 일일이 치지 않고 문자열로 단축해서 코딩할 수 있습니다.


4. 질의와 응답

한 코드를 인터프리터가 해석하면 질의를 받아 응답할 수 있습니다.

질의받은 식의 각 변수에 어떤 값을 배정할 때 그 식이 유도될 수 있는지를 답합니다.

예를 들어 "Main( 'ssz' )?"라고 질의하면 

  1. +
라고 답합니다. 유도할 수 없는 것으로 증명되면 "-"라고 답합니다. 한편 "Main( a )?"라고 질의하면 다음과 같이 답합니다.
  1. + a → 'z'.
  2. ▶ a → 's' Nat1.
  3. ▶+ Nat1 = a.
a → 'z'일 때 유도될 수 있고
a → 's' Nat1일 때는
Nat1 = a이면 유도될 수 있다.
라는 뜻입니다.