cs/pl/ppl/topic1/

[giscus[bot]]

cs/pl/ppl/topic1/

鹤翔万里（TonyCrane）的笔记本

https://note.tonycrane.cc/cs/pl/ppl/topic1/

[HobbitQia]

kami

[cubicYYY]

我喜欢你

[cubicYYY]

笔记：
如何定义乘法？下面给出一个例子。
加法plus的本质是将 $n+m$ 理解为把 $n$ 作为原点 $z$ ，往后求 $m$ 次后继succ.
类比通过复合succ算子构造加法plus，我们可以基于刚刚得到的plus算子来构造乘法mul（这很meta）
本质上，我们有 $m=1*m$，因此只需要每次步进从1改为 $n$ 即可变成乘法，也就是把自然数定义中的 $s$ 改为 $(N\ s)$ ：
$mul:=\lambda N.\lambda M.\lambda s.\lambda z.M(N\ s)z$
对于指数exp， $m^n$ 只是把 $m$ 这个自然数复合了 $n$ 次。如果说上文的 $(N\ s)$ 是把 $s$ 复合了 $N$ 次，那么我们需要把 $M$ 复合 $N$次自然就是：
$exp:=\lambda M.\lambda N.N\ M$

[cubicYYY]

指数也可以从乘法推得，试试看设计 $M^1$ , $M^2$, ...的函数并观察其中 $s$ 部分是如何与自然数定义同构的