# Lecture 3

- So far
	- Reviosonf of inference rules, natural (rule) induction
	- First steps haskell
	- Simple grammers specified using inference rules
	- Started with concrete (What you see as a programmer)/abstract syntax (Focus on the essential)
- This week
	- First-order & higher-order syntax
	- Static and dynamic semantics

We write

e SExpr <-> t expr

iff the (concrete grammer) expression e correspond to the (abstract grammar) expression t.




- $$\frac{e \text{Bool}}{e\text{BExpr}},
\frac{e\text{BExpr}}{(e)\text{BExpr}},
\frac{e_1\text{Bexpr},e_2\text{BExpr}}{e_1\lor e_2\text{BExpr}},
\frac{e \text{BExpr}}{\neg e\text{BExpr}},
\frac{e_1\text{Bexpr},e_2\text{BExpr}}{e_1\land e_2\text{BExpr}}$$

- $\text{True} \lor \text{False} \land \text{True}$

- $$\frac{e \text{Bool}}{e\text{BExpr1}},
\frac{e\text{BExpr}}{(e)\text{BExpr1}},
\frac{e_1\text{Bexpr},e_2\text{BExpr3}}{e_1\lor e_2\text{BExpr}},
\frac{e \text{BExpr1}}{\neg e\text{BExpr2}},
\frac{e_1\text{Bexpr},e_2\text{BExpr2}}{e_1\land e_2\text{BExpr3}}$$
$$
\frac{e \text{BExpr1}}{e\text{BExpr2}},
\frac{e \text{BExpr2}}{e\text{BExpr3}},
\frac{e \text{BExpr3}}{e\text{BExpr}},
$$
- $$\frac{e \text{Bool}}{e P},\frac{eP}{(e)P},\frac{e_1P,e_2P}{e_1\land e_2 P},\frac{eP}{\neg eP}$$


$$\frac{s_1N}{s_1 M}$$


- Use the propery that it always starts with M. Then use the property that there is no I directly after U.