대칭 메타프로그래밍의 메타이론
대칭 메타프로그래밍의 메타이론 (The Meta-theory of Symmetric Metaprogramming)
이 노트는 원칙적인 메타프로그래밍의 단순화된 변형을 제시하고 그 타당성(soundness) 증명의 골자를 설명해요. 두 스테이지 사이의 대화만을 다루는 변형이에요. 프로그램은 splice를 담을 수 있는 quote를 가질 수 있어요(그리고 quote를 담을 수 있는 splice, 계속 반복). 또는 프로그램이 splice로 시작해서 quote가 내장될 수도 있어요. 핵심 제한은 (1) term이 최상위 quote 또는 최상위 splice를 포함할 수 있지만 둘 다는 안 되고, (2) quote가 직접 quote 안에, splice가 직접 splice 안에 나타날 수 없다는 거예요. 다른 말로, 우주가 오직 두 개의 단계(phase)로 제한돼요.
본문
이 제한 아래에서 우리는 타입 규칙을 단순화할 수 있어서, 환경 스택 대신 항상 정확히 두 개의 환경이 있게 돼요. 여기서 제시하는 변형은 평가 문맥을 문맥적 타입 규칙으로 바꾼다는 점에서 완전한 계산과도 달라요. 이는 조금 더 장황하지만, 메타이론을 세우기 더 쉽게 만들어 줘요.
문법 (Syntax)
Terms t ::= x variable
(x: T) => t lambda
t t application
’t quote
~t splice
Simple terms u ::= x | (x: T) => u | u u
Values v ::= (x: T) => t lambda
’u quoted value
Types T ::= A base type
T -> T function type
’T quoted type
연산적 시맨틱 (Operational semantics)
평가 (Evaluation)
((x: T) => t) v --> [x := v]t
t1 --> t2
---------------
t1 t --> t2 t
t1 --> t2
---------------
v t1 --> v t2
t1 ==> t2
-------------
’t1 --> ’t2
스플라이싱 (Splicing)
~’u ==> u
t1 ==> t2
-------------------------------
(x: T) => t1 ==> (x: T) => t2
t1 ==> t2
---------------
t1 t ==> t2 t
t1 ==> t2
---------------
u t1 ==> u t2
t1 --> t2
-------------
~t1 ==> ~t2
타입 규칙 (Typing Rules)
타입 판정(typing judgment)은 E1 * E2 |- t: T 형태를 가져요. 여기서 E1, E2는 환경이고 *는 ~와 ’ 중 하나예요.
x: T in E2
---------------
E1 * E2 |- x: T
E1 * E2, x: T1 |- t: T2
--------------------------------
E1 * E2 |- (x: T1) => t: T -> T2
E1 * E2 |- t1: T2 -> T E1 * E2 |- t2: T2
-------------------------------------------
E1 * E2 |- t1 t2: T
E2 ’ E1 |- t: T
-----------------
E1 ~ E2 |- ’t: ’T
E2 ~ E1 |- t: ’T
----------------
E1 ’ E2 |- ~t: T
(흥미롭게도, 이건 크리스마스 트리처럼 보이네요.)
타당성 (Soundness)
메타이론은 보통 두 판정에 대한 상호 귀납(mutual induction)을 요구해요.
진행 정리 (Progress Theorem)
E1 ~ |- t: T라면, 어떤 값v에 대해t = v이거나, 어떤 termt2에 대해t --> t2이거나 둘 중 하나예요.’ E2 |- t: T라면, 어떤 단순 termu에 대해t = u이거나, 어떤 termt2에 대해t ==> t2이거나 둘 중 하나예요.
증명은 term에 대한 구조적 귀납으로 해요.
(1)을 증명하려면:
- 변수, 람다, 애플리케이션의 case는 STLC와 같아요.
t = ’t2라면, 역전(inversion)에 의해 어떤 타입T2에 대해’ E1 |- t2: T2가 있어요. 두 번째 귀납 가설(I.H.)로 우리는 다음 중 하나를 얻어요:t2 = u, 따라서’t2는 값이에요.t2 ==> t3, 따라서’t2 --> ’t3이에요.
t = ~t2case는 타입 부여가 불가능해요.
(2)를 증명하려면:
t = x라면t는 단순 term이에요.t = (x: T) => t2라면,t2가 단순 term일 수 있는데, 그 경우t도 단순 term이에요. 또는 두 번째 I.H.로t2 ==> t3인데, 그 경우t ==> (x: T) => t3이에요.t = t1 t2라면 다음 세 case 중 하나가 적용돼요:t1과t2가 단순 term이면,t도 단순 term이에요.t1이 단순 term이 아니면, 두 번째 I.H.로t1 ==> t12이므로t ==> t12 t2이에요.t1은 단순 term이지만t2가 아니면, 두 번째 I.H.로t2 ==> t22이므로t ==> t1 t22이에요.
t = ’t2case는 타입 부여가 불가능해요.t = ~t2라면, 역전에 의해 어떤 타입T2에 대해E2 ~ |- t2: ’T2가 있어요. 첫 번째 I.H.로 우리는 다음 중 하나를 얻어요.t2 = v.t2: ’T2이므로v = ’u(어떤 단순 termu에 대해)여야 해요. 따라서t = ~’u. quote-splice 축소로t ==> u이에요.t2 --> t3. 그러면’t에 대한 문맥 규칙으로t ==> ’t3이에요.
치환 보조정리 (Substitution Lemma)
E1 ~ E2 |- s: S이고E1 ~ E2, x: S |- t: T라면E1 ~ E2 |- [x := s]t: T이에요.E1 ~ E2 |- s: S이고E2, x: S ’ E1 |- t: T라면E2 ’ E1 |- [x := s]t: T이에요.
증명은 t에 대한 타입 유도에 대한 귀납으로 하고, STL 증명과 유사해요. (2)는 (1)보다 조금 단순한데, 람다 바인딩을 바운드 변수 x와 바꿀 필요가 없기 때문이에요. 두 가설을 연결하는 논거는 다음과 같아요.
(1)을 증명하려면, t = ’t1이라 하자. 그러면 어떤 타입 T1에 대해 T = ’T1이고 마지막 타입 규칙은 다음과 같아요.
E2, x: S ’ E1 |- t1: T1
-------------------------
E1 ~ E2, x: S |- ’t1: ’T1
두 번째 I.H.로 E2 ’ E1 |- [x := s]t1: T1. 타이핑으로 E1 ~ E2 |- ’[x := s]t1: ’T1. [x := s]t = [x := s](’t1) = ’[x := s]t1이므로 [x := s]t: ’T1을 얻어요.
(2)를 증명하려면, t = ~t1이라 하자. 그러면 마지막 타입 규칙은 다음과 같아요.
E1 ~ E2, x: S |- t1: ’T
-----------------------
E2, x: S ’ E1 |- ~t1: T
첫 번째 I.H.로 E1 ~ E2 |- [x := s]t1: ’T. 타이핑으로 E2 ’ E1 |- ~[x := s]t1: T. [x := s]t = [x := s](~t1) = ~[x := s]t1이므로 [x := s]t: T을 얻어요.
보존 정리 (Preservation Theorem)
E1 ~ E2 |- t1: T이고t1 --> t2라면E1 ~ E2 |- t2: T이에요.E1 ’ E2 |- t1: T이고t1 ==> t2라면E1 ’ E2 |- t2: T이에요.
증명은 평가 유도에 대한 구조적 귀납으로 해요. (1)의 증명은 STL 증명과 유사한데, 베타 축소 case에 치환 보조정리를 사용하고, quoted term의 축소가 추가돼요. 그것은 다음과 같이 진행돼요.
- 마지막 규칙이
t1 ==> t2
-------------
’t1 --> ’t2
이라고 가정해요.
타입 규칙의 역전으로, 어떤 타입 T1에 대해 t1: T1이 되는 T = ’T1이어야 해요. 두 번째 I.H.로 t2: T1, 따라서 ’t2:T1`이에요.
(2)를 증명하려면:
- 마지막 규칙이
~’u ==> u라고 가정해요.~’u의 타입 증명은 다음 형태를 가져야 해요.
E1 ’ E2 |- u: T
-----------------
E1 ~ E2 |- ’u: ’T
-----------------
E1 ’ E2 |- ~’u: T
따라서 E1 ’ E2 |- u: T이에요.
- 마지막 규칙이
t1 ==> t2
-------------------------------
(x: S) => t1 ==> (x: T) => t2
이라고 가정해요.
타입 역전으로, T = S -> T1이 되는 어떤 타입 T1에 대해 E1 ' E2, x: S |- t1: T1이에요. I.H.로 t2: T1. 람다 타입 규칙으로 결과가 따라와요.
- 애플리케이션에 대한 문맥 규칙은 똑같이 직접적이에요.
- 마지막 규칙이
t1 ==> t2
-------------
~t1 ==> ~t2
이라고 가정해요.
타입 규칙의 역전으로, t1: ’T이어야 해요. 첫 번째 I.H.로 t2: ’T, 따라서 ~t2: T이에요.