complement notes in 10.16

notes/5.md

@@ -8,12 +8,12 @@
 * inheritance relationships
 * single definition
 
-## Categories of Semantic Analysis
+There are two main categories of semantic analysis:
 
 * Scopes
 * Types
 
-### Scope
+## Scope
 
 **Lexical Scope**: textual region in the program
 
@@ -33,7 +33,7 @@ And program has hierachy of symbol tables(scope).
 
 if the identifier is used traverse the hierachy of symbol tables upward until finding the identifier with the same name to determine the declaration from the current scope.
 
-#### Build a Symbol Table
+### Build a Symbol Table
 
 there are five operations:
 * insert scope
@@ -42,7 +42,7 @@ there are five operations:
 * add symbol(x)
 * check scope(x)
 
-### Type
+## Type
 
 * Type checking
 * Type inferencing
@@ -56,3 +56,37 @@ Three Language Types:
 Does not require additional type checking instructions at runtime.
 and guarantees that the executions are safe at compile time.
 modern languages require both static and dynamic type checking(union, void ptr)
+
+So what is types?
+
+A type indicates a description of a set of values and a set of allowed operations on those values.
+* Type Expressions: Describe the possible typse in the program, e.g., `int`, `char*`, `array[]`, `object`.
+* Type System: Defines types for language constructs (think about nodes in AST)
+
+### Type Comparision Implementation
+
+1. Implement a method `Equals(T1, T2)`
+   * must compare type trees of `T1` and `T2`
+2. Use unique objects for each distinct type
+   * each type expression resolved to same type object everywhere
+   * faster type comparision(use `==`)
+   * object-oriendted: check subtyping of type objects
+
+for option 1
+
+### Type Checking Methodology
+
+
+
+### Inferecnce Rules
+
+### Soundness
+
+$$\frac{i\text{ is an integer literal}}{\vdash i: \texttt{int}}[\texttt{int}]$$
+
+Some rules are sound but not necessary for a language: (not giving meanings)
+
+$$\frac{i\text{ is an integer literal}}{\vdash i \text{ is object} }$$
+
+
+$$\frac{e_1: \texttt{bool} \quad e_2: T}{\vdash \texttt{while} (e_1) \{ e_2 \} : \texttt{void}}[\texttt{while}]$$