Prog1-Part2

感觉自己下半学期学的有点问题，写点笔记复习一下

感觉下半学期的重点是编译原理，主要可以分为这么几个部分：

1. Lexer: 把程序转化为Token
2. Parser: 把Token转化为语言的数据类型
3. Elaborator: 静态类型检查
4. Evaluator: 求值

自我感觉1.3.4.掌握的还行，Paser还是有点不明白。

以及3.4.的Derivation Tree还要再记一下表示方法。

编译原理这一块还是先拿课上的顺序进行整理：3.4.1.2.

编译原理

Elaborator——静态类型检查

作为人类，可能能一步一步推导类型，但怎么让计算机做呢？

仔细观察（bushi），可以抽象出来几条规则，这里拿latex抄一遍：

渲染有问题，直接用图片了QwQ

这个还是比较好理解的，因为不涉及环境的变更，一点一点推导下去就可以了。

Evaluator——动态求值

这里涉及环境的变更，所以语法上有些地方要注意。

1. 函数要写成Tuple的形式
2. 新的环境要在最后表示出来

函数在Abs时候要写成Tuple形式。

Lexer——Token化

这个没啥难的，直接字符串explode后match就可以

Parser——把Token处理为Eval和Elab能处理的形式

这里用的是Recursively Descending Parser
主要思想就是先处理优先级低的，然后一步一步向下处理。
这里用到了OCaml一个制造相互使用的函数的语法糖：and。
就是可以前面先用这个函数，然后and 函数名=…补上。

这里复习一下我一分不得的Mini Test题目：

type token=HE|HO|LP|RP|SIM
;;
type exp=He|Ho|Sim of exp*exp
;;
type cexp ts=
match pty ts with
| t1, SIM :: ts = let t2,ts = cexp ts in (Sim(t1,t2),ts)
| p->p
and pty = function
| HE::ts -> (He,ts)
| HO::ts -> (Ho,ts)
| LP::ts -> 
        let t1,ts = cexp ts in
        let ts = expect RP ts in
        (t1,ts)
| _->failwith "Not Valid"

核心还是每次解析的时候尝试看看下层还有没有可以解析的，然后一层一层向下。

核心就是Grammar，对每个非终结符总结一个替换方式然后按优先级逐个应用。

形式化的递归表达

现在课上在讲这个，顺手写一下吧。

递归式的一种表示方法

e.g.

$Fib(x) = \text{IF } x<2 \text{ THEN } x \text{ ELSE } Fib(x-1)+Fib(x-2)$

可以表示为 $\text{IF } x<2 \text{ THEN } \langle\rangle \text{ ELSE } \langle x-1,x-2\rangle$

递归关系

刚才的柿子中，$\langle\rangle$ 中的东西叫Precedent Argument. 如果我们把当前参数和Precedent Argument中间连一条有向边，就构成的一个递归关系R。

可以和之前的Termination Relation联系起来：你能terminate， 这个递归才能结束。怎么判断能否Terminate呢，看这个function能不能在某种encoding下countable。

证明函数定义和数学上的函数表达的是一个东西

这一部分主要是数学上的证明，跟编程知识就没啥关系了。

但是minitest里给出了需要的证明方式：

1.证明Dom something$\subseteq$Dom f

给出Termination Function， 证明两个Dom都对这个function terminate， 所以有这个关系

2.证明数学上一致

对每个条件分支，做一下和Mathematical induction类似的变形。

Structural Induction

Given a claim, for each possible arg, make the claim a induction form.

解题过程的注意事项

首先，起手式是固定的，以List相关内容为例：

Let $X$ be an arbitrary yet fixed type, we show the $\forall xs\in \mathcal{L}(X), ys\in \mathcal{L}(X),...\text{(the claim) by structural induction on } xs$

重点是arbitrary but fixed以及全称量词的使用.
然后开始induction，先证基本类型，再证induction的part。
重点就是要写得尽可能详细，每一步都要有出处，常见的有：

• arithmetic
• a=b+c
• IH(induction hypothesis)
• Definition of function
• …

Prog1的time complexity

Size function revisited

注意这个东西的选择。如果你给一个$\mathcal{O}(n)$算法选择了形如$\lambda n\in \mathbb{N},2^n$的size function，那么你在主定理的柿子里就要用形如$T(n)=T(2^{\log_2n-1})+\mathcal{O}(\text{something})$的柿子。

主定理复习

对于形如

$$T(n)=b\cdot T(\frac{n}{a})+\mathcal{O}(n^d\log^s n)$$

$$f(n)=n^d\log^s n$$

的柿子，有：

1. $a<b^d, \mathcal{O}(n^d\log^s n)$
2. $a=b^d,\mathcal{O}(n^d\log^{s+1}n)$
3. $a>b^d,\mathcal{O}(n^{\log_b a})$

在Prog1里，$T(n)$被替换成了$t\space n$的形式，$f(n)$被替换成了$co\space n$的形式。做题的时候要小心一点。

解题格式

在mini test中给出：

1. 写出size function。
2. 写出主定理的形式。
3. 给出复杂度。