Semantic Analysis - 2

* Static Semantics

프로그램에서 사용되는 타입을 기술하는 언어이고, 타입 체킹을 어떻게 할 것인지 기술하는 방법이다.

Syntax analysis 에서 CFG, lexical analysis 에서 regular expression 과 같다고 생각하면 된다.

 

타입을 판단하는 방법에 대해 formal 하게 표현하는 방법을 말하는데, E : T 로 정의된다. 이는 E 는 T 라는 타입으로 호환된다는 것을 말한다.

 

> Type judgement 의 예는 다음과 같다.

   - 2 : int

   - true : bool

   - 2 * (3+4) : int

   - "hello" : string

 

> 구문 (statement) 에 대한 type judgement 

   - if (b) 2 else 3 : int

   - x == 10 : bool

   - b = true, y = 2 : int ( , operator 가 있으면 마지막 구문을 결과로 한다.)

 

> 수식이 아닌 경우에는 스페셜 유닛 타입을 지정하는데, S : unit 으로 표현하고 이는 어떠한 S 가 어떠한 result type 으로도 well-type 되지 않는다는 것을 의미한다.

 

 

 

* Deriving a Judgement

앞 예제 if (b) 2 else 3 : int 를 다시 보자.

int type 으로 well-typed 되려면 어떤 조건이 필요한지 생각해야 한다. b 는 bool, 2 는 int, 3은 int 가 될 때 well-type 된다.

 

 

 

* Type Judgements

Type judgement 를 위해 A 개념을 추가하는데, context 라고 한다.

A ⊢ E : T  형태로 표기하는데, 이는 context A 에서 expression E 가 type T 로 well-type 됨을 의미한다. A는 context 니까 현재 시스템에서 알 수 있는 상황이 들어간다. 즉, type context ( = symbol table 에 들어가 있는 정보들) 이고, 이는 type binding ( id : T ) 의 set 이다. 

 

 

그렇다면 다음 예제가 이해될 것이다. 

b가 bool 이고 x가 int 일 때 결과로 읽을 수 있다.

- b : bool, x : int ⊢ b : bool 

- b : bool, x : int ⊢ if (b) 2 else x : int

                            ⊢ 2 + 2 : int

 

 

또 다른 예로, A ⊢ if (E) S1 else S2 : T 에서 true 가 되는 조건은 무엇일까?

바로 다음과 같은데,

A ⊢ E : bool

A ⊢ S1 : T

A ⊢ S2 : T

이는 A 에서 E 가 bool 이고, S1 이 T고, S2 가 T이면 judgement 가 참임을 알 수 있다. 

 

 

 

* Inference Rules

정리해서 추론 룰을 보자.

전제가 참이면 결론이 참이다. 

 

 

> 왜 추론 룰이 필요할까? static sematics 를 specifying 하기 위한 간단한 언어이다. 또, 실제 AST (Abstract Syntax Tree) 를 traversal 하면서 나오는 것이기 때문에 그 순서대로 추론할 수 있다. 타입 체킹은 추론 룰을 거꾸로 돌면서 문제가 없음을 알아보는 것이다.

 

 

 

 

 

* Proof Tree

Type judgement (A ⊢ E : T ) 가 참인지 알아보기 위해 추론 룰을 거꾸로 찾아가는 것을 말한다. type judgement 에 대한 type derivation 이 존재할 때 Expression 이 well-type 이라고 하고, type derive 과정을 proof tree 라고 한다. 

다음과 같이 proof tree 를 보일 수 있다. 

if A1 = b : bool, x : int 를 보고 전제를 할 수 있고, 이를 바탕으로 결론이 참이 됨을 도출할 수 있다.

 

 

 

 

 

 

총 정리하자면,

static sematics 는 타입 체킹 룰을 spec 으로 저장할 수 있는 방법이고, 수식이나 구문은 추론 룰을 이용해 proof tree 를 만들 수 있으면 well-typed 임을 알 수 있다. 만들 수 없으면 타입 에러가 있는 구문이거나 수식이다.

 

sematic analysis 는 lexical 과 syntax analysis 로 찾지 못한 에러를 확인하는 것이고, 크게 scope error (변수가 정의되지 않았거나 여러번 선언된 경우) 와 type error 로 나뉜다.