add syntax

notes/4.md

@@ -68,3 +68,77 @@ Language usually have basic types aka primitive types. Using these types to buil
 There are two options:
 1. Implement a method `Equals(T1, T2)`.
 It must compare type trees of T1 and T2. For OOP languages also need sub-types
+
+
+### Type Checking Methodology
+Type checking means verifying whether expressions are given proper types
+1. Implement using Syntax-Directed Definitions(SDD)
+2. First build the AST, then implement type checking by recursive traversal of the AST nodes
+
+#### SDD
+
+SDD associates semantic rules for the productions in the CFG. It checks types based on the semantic rules associated with the production rules.
+
+#### AST Traversal
+
+Type Checking During AST Traversal.
+
+중간에 새로운 타입이 생길 수 있음.
+
+By Recursive Traversal of the AST nodes, inferencing types of AST nodes.
+
+### Inference
+
+$$\frac{\vdash H_1 \vdash H_2 \vdash H_3}{\vdash \text{conclusion}}[\text{rule name}]$$
+
+#### Soundness
+
+항상 참이 되는 타입
+
+$e : T$ means that $e$ is a sound expression of type $T$, that is $e$ is always the type $T$.
+
+for non expression statements use special unit type (like void or empty type)
+
+$S: \text{void}$
+
+#### Proof Tree
+
+$$\frac{
+  \frac{1 \text{ is a integer literal}}{\vdash 1: \text{int}} [\text{int}] \;
+  \frac{2 \text{ is an integer literal}}{\vdash 2: \text{int}} [\text{int}]
+  }{\vdash 1 + 2 : \text{int}} [\text{int add}]
+  $$
+
+Proof Tree는 AST를 뒤집은 모양.
+
+If-then-else는 가질 수 있는데, If-then은 타입을 가질 수 없음.
+
+
+
+#### Type Environment
+
+어떻게 $x$가 variable이라고 할때 어떤 타입을 가지는지 알 수가 없음.
+
+Type Environment gives types for **free variables**.
+
+$$O \vdash e: T$$
+* $O$ is essentially **symbol table**.
+
+Complex Example of Declaration:
+```c
+for (T1 i = 0;;) {
+  exp
+}
+```
+$$\frac{O[T1/i] \vdash \text{exp}: T2}{O\vdash \texttt{for}(i: T1) \set{\text{exp}: T2}}$$
+
+Complex Example of Class Attrs
+
+$$O_C(x) = T$$
+* forall attrs $x: T$ in class C
+$$O_C$$
+
+Complex Example of Class Methods
+
+### Subtyping
+