# Mingjian's Blog

You are just a hardcore character of the life game. Keep upgrading and don't die.

0%

AST是Abstract Syntax Trees的缩写, 中文是抽象语法树.

## AST和code的转换

python代码有三个分身,

1. 以unicode字符串存在的源代码. 人类可读写, python解释器不可读.
2. 以AST对象存在的抽象语法树. 人类可读写, 但很难读懂原来的语义, 用来显示python语义元素之间的关系. 是从源代码翻译成目标代码的中间产品.
3. 以code object存在的可执行的目标代码. python解释器可读, 人类不可读.

$$\def\tauequ{\mathbin{\vDash\style{display: inline-block; transform: scaleX(-1)}{\vDash}}}$$ $$\def\Dashv{\mathbin{\style{display: inline-block; transform: scaleX(-1)}{\vDash}}}$$ $$\def\DEF{\sf{D\scriptsize EF}.\quad}$$ $$\def\DEFi{\sf{D\scriptsize EF}^*.\quad}$$ $$\def\DEFn{\sf{D\scriptsize EF}_*.\quad}$$ $$\def\DEFin{\sf{D\scriptsize EF}^*_*.\quad}$$ $$\def\llbracket{\unicode{x27E6}}$$ $$\def\rrbracket{\unicode{x27E7}}$$ $$\def\PROOF{\sf{P\scriptsize ROOF}.\quad}$$

##### Problem 1

Show that (a) $$\Gamma;\alpha\vDash\varphi$$ iff $$\Gamma\vDash(\alpha\rightarrow\varphi)$$; and (b) $$\varphi\tauequ\psi$$ iff $$\vDash(\varphi\leftrightarrow\psi)$$.

$$\PROOF$$

$$\def\PROOF{\sf{P\scriptsize ROOF}.\quad}$$

##### Problem 2

Show that no one of the following sentences is logically implied by the other two. (This is done by giving a structure in which the sentence in question is false, while the other two are true.)

1. $$\forall{x}\forall{y}\forall{z}(Pxy\rightarrow Pyz\rightarrow Pxz).$$ Recall that by our convention $$\alpha\rightarrow\beta\rightarrow\gamma$$ is $$\alpha\rightarrow(\beta\rightarrow\gamma).$$
2. $$\forall{x}\forall{y}(Pxy\rightarrow Pyx\rightarrow x=y).$$
3. $$\forall{x}\exists{y}Pxy\rightarrow\exists{y}\forall{x}Pxy.$$

$$\def\tauequ{\mathbin{\vDash\style{display: inline-block; transform: scaleX(-1)}{\vDash}}}$$ $$\def\Dashv{\mathbin{\style{display: inline-block; transform: scaleX(-1)}{\vDash}}}$$ $$\def\DEF{\sf{D\scriptsize EF}.\quad}$$ $$\def\DEFi{\sf{D\scriptsize EF}^*.\quad}$$ $$\def\DEFn{\sf{D\scriptsize EF}_*.\quad}$$ $$\def\DEFin{\sf{D\scriptsize EF}^*_*.\quad}$$ $$\def\llbracket{\unicode{x27E6}}$$ $$\def\rrbracket{\unicode{x27E7}}$$ $$\def\PROOF{\sf{P\scriptsize ROOF}.\quad}$$

$$\def\tauequ{\mathbin{\vDash\style{display: inline-block; transform: scaleX(-1)}{\vDash}}}$$ $$\def\Dashv{\mathbin{\style{display: inline-block; transform: scaleX(-1)}{\vDash}}}$$ $$\def\DEF{\sf{D\scriptsize EF}.\quad}$$ $$\def\DEFi{\sf{D\scriptsize EF}^*.\quad}$$ $$\def\DEFn{\sf{D\scriptsize EF}_*.\quad}$$ $$\def\DEFin{\sf{D\scriptsize EF}^*_*.\quad}$$ $$\def\llbracket{\unicode{x27E6}}$$ $$\def\rrbracket{\unicode{x27E7}}$$ $$\def\PROOF{\sf{P\scriptsize ROOF}.\quad}$$

$$\def\tauequ{\mathbin{\vDash\style{display: inline-block; transform: scaleX(-1)}{\vDash}}}$$ $$\def\Dashv{\mathbin{\style{display: inline-block; transform: scaleX(-1)}{\vDash}}}$$ $$\def\DEF{\sf{D\scriptsize EF}.\quad}$$ $$\def\DEFi{\sf{D\scriptsize EF}^*.\quad}$$ $$\def\DEFn{\sf{D\scriptsize EF}_*.\quad}$$ $$\def\DEFin{\sf{D\scriptsize EF}^*_*.\quad}$$

$$\def\tauequ{\mathbin{\vDash\style{display: inline-block; transform: scaleX(-1)}{\vDash}}}$$ $$\def\Dashv{\mathbin{\style{display: inline-block; transform: scaleX(-1)}{\vDash}}}$$ $$\def\DEF{\sf{D\scriptsize EF}.\quad}$$ $$\def\DEFi{\sf{D\scriptsize EF}^*.\quad}$$ $$\def\DEFn{\sf{D\scriptsize EF}_*.\quad}$$ $$\def\DEFin{\sf{D\scriptsize EF}^*_*.\quad}$$