---
tags: FLOLAC, Logic, Language, Computation, Functional Programming
---
FLOLAC '18
=
Formosan Summer School on Logic, Language, and Computation
今年在台大為 3 學分的課, 註冊課名 「程式語言理論與型態系統」
「偶數年」為基礎的 Functional Programming 必備的知識
「奇數年」之主題為形式化驗證，課名 「自動化正規驗證」[^1]
==在本文我只提及我覺得挺有趣的部份，這些並不是課程的全部==
詳細課程內容，可以到 [FLOLAC' 18 的課程網站](http://flolac.iis.sinica.edu.tw/flolac18/courses.html)下載投影片窺見
# Evaluation?
在 haskell 中做 $(3 + 4)^2$ 的求值(或著說 化簡(simplifying)， 規約(reducing))
可以想像會有以下兩種形式
Applicative order evaluation:
```haskell
square (3 + 4)
= { definition of + }
square 7
= { definition of square }
7 * 7
= { definition of * }
49
```
Normal order evaluation:
```haskell
square (3 + 4)
= { definition of square }
(3 + 4) * (3 + 4)
= { definition of + }
7 * (3 + 4)
= { definition of + }
7 * 7
= { definition of * }
49
```
想想看 每當我們對一個算式做不同的求值順序，最終總會得到相同的東西嗎?
# Propositional Logic
給定一個 $\text{PV}$ 作為 propositional variable names 的集合
$\text{PV} \subseteq \text{Prop}$
$\bot \in \text{Prop}$
if $\phi, \psi \in \text{Prop}$, then $\phi \land \psi$, $\phi \lor \psi$, and $\phi \to \psi \in \text{Prop}$
## Natural deduction
$$
\frac {
\frac {} {
\frac {
(A \land B)\vdash (A \land B)
} {
(A \land B)\vdash B
} (\land \text{ER})
} (\text{a})
\hspace{1cm}
\frac {} {
\frac {
(A \land B)\vdash (A \land B)
} {
(A \land B)\vdash A
} (\land \text{EL})
} (\text{a})
} {
\frac {
(A \land B)\vdash (B \land A)
} {
\vdash (A \land B) \to (B \land A)
} (\to \text{I})
} (\land \text{I})
$$
有用的 deduction system 必須要能分辨什麼是能證和不可證的，畢竟如果萬物皆可證，那我們也不用證明了。
## Sequent
$$\Gamma\vdash\Sigma$$
他的前件 $\Gamma$ 是按照 $\cap$ 來解釋的，而後件 $\Sigma$ 則是 $\cup$
通俗的說，當把這個 Sequent 寫下來，代表有一堆有證明的 assumption $\Gamma$，我們希望有 $\Sigma$ 這個結論
而證明這個 Sequent 的工具就是 Deduction System
特別的是當寫 $\vdash\Sigma$ 代表不需要任何 assumption， $\Sigma$ 自動成立，這叫做 **Theorem**
## Rule
在 natural deduction 中一個 sequent 叫做 $J$udgement
而 rule 是以下形式：
$$
{J_1\hspace{0.5cm} J_2\hspace{0.5cm} ...\hspace{0.5cm} J_n\over J}(\text{name})
$$
> there are three different levels of implication: $\to$ in a proposition, $\vdash$ in a judgement, and the line in a rule.
### Assumption
$$
{\over\Gamma\vdash\phi}(\text{assum})
$$
side condition: 當 $\phi$ 也出現在 $\Gamma$ 中。
### Conjunction
Introduction:
$$
{\Gamma\vdash\phi\quad\quad\Gamma\vdash\psi\over\Gamma\vdash\phi\land\psi}(\land \text{I})
$$
Elimination:
$$
{\Gamma\vdash\phi\land\psi\over\Gamma\vdash\phi}(\land \text{EL})
\quad\quad\quad\quad\quad
{\Gamma\vdash\phi\land\psi\over\Gamma\vdash\psi}(\land \text{ER})
$$
### Implication
Introduction:
$$
{\Gamma,\phi\vdash\psi\over\Gamma\vdash\phi\to\psi}(\to \text{I})
$$
Elimination:
$$
{\Gamma\vdash\phi\to\psi\quad\quad\Gamma\vdash\phi\over\Gamma\vdash\psi}(\to \text{E})
$$
### Disjunction
Introduction:
$$
{\Gamma\vdash\phi\over\Gamma\vdash\phi\lor\psi}(\lor \text{IL})
\quad\quad\quad\quad\quad
{\Gamma\vdash\psi\over\Gamma\vdash\phi\lor\psi}(\lor \text{IR})
$$
Elimination:
$$
{\Gamma\vdash\phi\lor\psi\quad\quad\Gamma,\phi\vdash\vartheta\quad\quad\Gamma,\psi\vdash\vartheta\over\Gamma\vdash\vartheta}(\lor \text{E})
$$
### Falsity
Introduction: none
Elimination:
$$
{\Gamma\vdash\bot\over\Gamma\vdash\phi}(\bot \text{E})
$$
通常使用 $\neg\phi$ 表示 $\phi \to \bot$
以及 $\top$ 表示 $\bot \to \bot$
> 我猜想，$\bot$ 就相當於整個 Prop set
作業兩題: [A Feast of double negation](http://flolac.iis.sinica.edu.tw/flolac18/files/logic/logic-homework-solution.pdf) 做得有夠久，但是挺有意思的
期末考題：
Derive $A \lor(B\land C) \vdash (A\lor B)\land (A\lor C)$.
# Intuitionistic vs Classical
可以藉由加入以下兩條規則到 $\text{NJ}$ 中來得到 classical logic 的 deduction system $\text{NK}$
$$
{\over\Gamma\vdash\phi\lor\neg\phi}(\text{LEM})\quad\quad\quad{\Gamma\vdash\neg\neg\phi\over\Gamma\vdash\phi}(\neg\neg \text{E})
$$
在 Intuitionistic logic 中, $\neg\neg A$ 與 $A$ 是不同東西。
對於 Classical logic，他著重的點是一個命題非真即假(LEM)
>命題本身一旦被視為真實，不管處在哪個環境下他都為真實的
例如一個問題：
$\exists x, y \in \mathbb{R}\backslash\mathbb{Q}$ s.t. $x^y \in \mathbb{Q}$
(關於 [$\exists$ 存在量詞](#existsxist))
若 $\sqrt{2}^\sqrt{2} \in \mathbb{Q}$ 則 $x = y = \sqrt{2}$ 否則 $x = \sqrt{2}^\sqrt{2}, y = \sqrt{2}$
根據 LEM，得證。
但這樣我們還是沒辦法知道哪個情況是正確(?)的，在 Intuitionistic logic 我們這樣做：
let $x = \sqrt{2}, y = 2\times \log_2 3$ then $x^y = 3$
> 所有的邏輯系統都存在破綻
# Classical semantics of propositional logic
$[\_]:Prop \to (PV \to \textbf{2})\to\textbf{2}$ where $\textbf{2}:=\{0, 1\}$
$[\bot] \sigma = 0$
$[v:PV] \sigma = \sigma v$
$[\phi\land\psi] \sigma = min([\phi]\sigma)([\psi]\sigma)$
$[\phi\lor\psi] \sigma = max([\phi]\sigma)([\psi]\sigma)$
$[\phi\to\psi] \sigma =$ if $[\phi]\sigma\leq[\psi]\sigma$ then $1$ else $0$
## Meta-connectives
lemma. $[\top]\sigma = 1$ for any valuation $\sigma$
以下採用 Structrued proof
[ASSUME] $\sigma:PV\to\textbf{2}$
[GOAL] $[\top]\sigma = 1$
[PROOF] Expand the definitions:
$$
\begin{split}
&\quad[\top]\sigma \\
&= \{ \text{definition of }\top \} \\
&\quad[\bot \to \bot]\sigma \\
&= \{ \text{definition of }[\_] \text{ for }\to \} \\
&\quad\text{if } [\bot]\sigma\leq[\bot]\sigma \text{ then } 1 \text{ else } 0 \\
&= \{ \text{definition of }[\_] \text{ for }\bot \} \\
&\quad\text{if } 0\leq0 \text{ then } 1 \text{ else } 0 \\
&= \{ 0 \leq 0\} \\
&\quad1
\end{split}
$$
## Deduction system vs classical semantics
Theorem. NK is **sound** with respect to the classical semantics:
$\Gamma\vdash_{\text{NK}} \phi$ implies $\Gamma \vDash \phi$
而因為所有 NJ derivation 都是一個 NK derivation，而有：
$\Gamma\vdash_{\text{NJ}} \phi$ implies $\Gamma \vDash \phi$
Theorem. NK is **complete** with respect to the classical semantics:
$\Gamma\vDash \phi$ implies $\Gamma \vdash _{\text{NK}} \phi$
但 NJ 不是 complete，例如排中律(LEM)雖然在 classical semantics 是 valid 但在 NJ 是不能做 derivation 的。
# First-order logic
if $v\in \mathbb{V} = \{a, b, c, ...\}$ then: $v \in \text{Term}_F$
if $t_1 ... t_n \in \text{ Term}_F$ then:
for any $f \in F$ with arity n, $f\hspace{0.1cm} t_1 ... t_n \in \text{ Term}_F$
$\text{P}$ is predicate symbols set, $\text{F}$ is function symbols set.
let signature $S = (\text{P}, \text{F})$, set $\text{ Form}_S$ of **first-order formulas** is:
$\bot\in \text{Form}_S$
if $t_1 ... t_n \in \text{ Term}_F$ then:
for any $p/n \in \text{P}$, $p\hspace{0.1cm}t_1 ... t_n \in \text{ Form}_S$
if $\phi, \psi\in \text{ Form}_S$ then:
$\phi \land \psi, \phi \lor \psi, \phi \to \psi \in \text{ Form}_S$
if $\phi\in \text{ Form}_S$, $v \in \mathbb{V}$ then:
$\forall v.\phi, \exists v.\phi \in \text{ Form}_S$
例如：
let $\text{P} := \{\text{Eq}/2\}$ and $\text{F} := \{\text{zero}/0, \text{suc}/1, \text{add}/2\}$
某命題： for every $x$, if $x \not= 0$ then there exists $y$ such that $\text{ suc } y = x$
可以寫成： $\forall x.\neg(\text{Eq } x \text{ zero}) \to \exists y.\text{Eq }(\text{suc }y)\hspace{0.1cm}x$
>Term 裡的東西碰上 predicate symbols 使他成為 propositions，之後就跟 propositional logic 很像了，只是多加了兩條規則。
## for $\forall$ll
Introduction:
$$
{\Gamma\vdash\phi\over\Gamma\vdash\forall v.\phi}(\forall I)
$$
其中 $v \notin \text{FV}(\Gamma)$
Elimination:
e.g. **所有**的貓都是動物。 t 是一隻貓，所以 t 是動物
$$
{\Gamma\vdash\forall v.\phi\over\Gamma\vdash\phi[t/v]}(\forall E)
$$
## $\exists$xist
Introduction:
e.g. 一隻叫 t 的貓喜歡打滾，所以**某一些**貓喜歡打滾
$$
{\Gamma\vdash\phi[t/v]\over\Gamma\vdash\exists v.\phi}(\exists I)
$$
Elimination:
$$
{\Gamma\vdash\exists v.\phi\quad\quad\Gamma,\phi\vdash\psi\over\Gamma\vdash\psi}(\exists E)
$$
其中 $v \notin \text{FV}(\Gamma) \cup \text{FV}(\psi)$
(關於 [$\text{FV}$ 的概念](#alpha-conversion))
# Induction on Natural Numbers
> 就是 Mathematical Induction
* P 0 holds
* P (1 + n) holds provided that P n does
這裡可以簡單的把 P (predicate) 看作：
```haskell
P :: Nat -> Bool
```
但最好別總是這麼想 (?
### Example: $(\text{map } f) \circ(\text{map } g) = \text{map } (f\circ g)$
P 0:
```haskell
(map f . map g) []
= { definition of composition }
map f (map g [])
= { definition of map}
map f []
= { definition of map }
[]
= { definition of map }
map (f . g) []
```
P (1 + n):
```haskell
(map f . map g) (x:xs)
= { definition of composition }
map f (map g (x:xs))
= { definition of map }
map f (g x : map g xs)
= { definition of map }
f (g x) : map f (map g xs)
= { definition of composition }
(f . g) x : (map f . map g) xs
= { induction with P n }
(f . g) x : map (f . g) xs
= { definition of map }
map (f . g) (x:xs)
```
(關於 [map 的定義](#Abstruction))
有人可能問： P n 難道不用證嗎？
當然要，不過我們可以用跟 P (1+n) 一樣的手法證明他，然後最後就會在已經證好的 P 0 停下。
# Coinduction
haskell 有個構造無限長的 List 的方式：
```haskell
Prelude> [1..]
[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33^CInterrupted.
```
即便他停不下來，依然能夠用 coinduction 的方式證明他的正確性
```haskell
iterate :: (a -> a) -> a -> [a]
iterate f e = e : iterate f (f e)
```
:::info
TODO: proof
:::
`[1..]` 等同於 `iterate (+1) 1`
# Peano axioms
## Example: 1 + 1 = 2
[Logic lecture 3 Page 23](http://flolac.iis.sinica.edu.tw/flolac18/files/logic/lecture_3.pdf) (這裡寫不下，可以進去好好觀賞一下)
# Meta-Language and Object-Language
Meta-Language 是用來描述 Object-Language 的一個 Language
> 就像是我們在用 haskell 寫證明一樣
參見： [Re: [其他] 邏輯中的"定義"該怎麼寫？](https://www.ptt.cc/bbs/Math/M.1366242723.A.7A4.html)
# Terms of $\lambda$-calculus
>柯向上的投影片左上角寫著： 一$\lambda$當千。真有趣(
let $\mathbb{V} := {a, b, c, ...}$ be a infinite set of variables, $\Lambda$ set is defined by:
variable 也是 lambda-term:
$$
{x \in \mathbb{V}\over x \in \Lambda}(\text{var})
$$
application (左結合):
> 剛學時對於左結合沒放上心，導致化簡時一直出錯QQ
$$
{M \in\Lambda\hspace{1cm} N \in\Lambda\over (MN) \in \Lambda}(\text{app})
$$
abstraction (右結合):
$$
{M \in\Lambda\hspace{1cm} x \in \mathbb{V}\over \lambda \hspace{0.1cm} x.M \in \Lambda}(\text{abs})
$$
## $\alpha$-conversion
> 就是有人會濫用同樣的變數名稱 (
$$
\begin{split}
&\lambda \hspace{0.1cm}x.x \not= \lambda \hspace{0.1cm}y.y \text{ but } \lambda\hspace{0.1cm} x.x \equiv_\alpha \lambda \hspace{0.1cm}y.y \\
&\lambda \hspace{0.1cm}x.\lambda \hspace{0.1cm}y.y \equiv_\alpha \lambda \hspace{0.1cm}z. \lambda \hspace{0.1cm}y.y \equiv_\alpha \lambda \hspace{0.1cm}z.\lambda\hspace{0.1cm} p.p \\
&\lambda\hspace{0.1cm} x.\lambda\hspace{0.1cm} y.bx \not\equiv_\alpha\lambda \hspace{0.1cm}x.\lambda \hspace{0.1cm}y.tx
\end{split}
$$
$\alpha$-conversion 將 受參數 bound 的變數換個名字
那些沒有 bounded 的變數稱為 free variables ($\text{FV}$)
$$
\begin{split}
&\text{FV}(x) = \{x\}\\
&\text{FV}(\lambda\hspace{0.1cm} x.M) = \text{FV}(M)\backslash \{x\}\\
&\text{FV}(MN) = \text{FV}(M) \cup \text{FV}(N)
\end{split}
$$
不是在 $\text{FV}$ 的變數們是 fresh 的：
$$
\lambda\hspace{0.1cm} x.M \to_\alpha \lambda \hspace{0.1cm}y.M[x \mapsto y] \text{ if y is fresh for M.}
$$
其中 $\mapsto$ 是變數變換。
## $\beta$-reduction
> 對於特殊的 lambda application 我們可以做點事
$\beta$-redex: ($\lambda \hspace{0.1cm}x.M)N$
$\beta$-reduction example: $(\lambda\hspace{0.1cm} x\hspace{0.1cm}y.x)MN \to_\beta (\lambda \hspace{0.1cm}y.M)N$
把 $\lambda$ 到 $.$ 之間的看作函數參數，application 的右邊代進去，就是在做 reduction
參見 ：[Introduction to Lambda Calculus](http://www.cs.ru.nl/~herman/onderwijs/provingwithCA/lambda-sel.pdf)
# Church Encoding of Natural Numbers
Church numerals:
$$
\begin{split}
c_0 &:= \lambda fx.x \\
c_1 &:= \lambda fx.fx \\
c_{n+1} &:= \lambda fx.f(f^nx)\\
\end{split}
$$
Successor:
$$
\begin{split}
&\text{succ}:= \lambda n.\lambda fx.f(nfx) \\
&\text{succ } c_n \to_{\beta^*} c_{n+1}
\end{split}
$$
Predecessor:
$$
\begin{split}
\text{pred } c_{n+1} \to_{\beta^*} c_{n}
\end{split}
$$
Addition:
$$
\begin{split}
&\text{add} := \lambda nm.\lambda fx.mf(nfx) \\
&\text{add } c_n\hspace{0.1cm}c_m \to_{\beta^*} c_{n+m}
\end{split}
$$
Condition:
$$
\begin{split}
&\text{ifz} := \lambda \hspace{0.1cm}n\hspace{0.1cm}x\hspace{0.1cm}y.n(\lambda \hspace{0.1cm} z.y)x \\
&\text{ifz } c_0\hspace{0.1cm}M\hspace{0.1cm}N \to_{\beta^*} M \\
&\text{ifz } c_n\hspace{0.1cm}M\hspace{0.1cm}N \to_{\beta^*} N
\end{split}
$$
附上期末考題：
reduce the term to its normal form using beta reduction closure ($\to_{\beta^*}$).
$$
(\lambda \hspace{0.1cm}n.n(\lambda\hspace{0.1cm} b.\lambda\hspace{0.1cm} x\hspace{0.1cm}y.byx)(\lambda\hspace{0.1cm} x\hspace{0.1cm}y.x)) c_{100}
$$
## Y combinator
Define (Curry's paradoxical combinator)
$$Y := \lambda\hspace{0.1cm} f.(\lambda\hspace{0.1cm} x.f(xx)) (\lambda\hspace{0.1cm} x.f(xx))$$
Then,
$$
\begin{split}
YF &\to_\beta (\lambda\hspace{0.1cm} x.F(xx)) (\lambda\hspace{0.1cm} x.F(xx)) \\
&\to_\beta F ((\lambda\hspace{0.1cm} x.F(xx)) (\lambda\hspace{0.1cm} x.F(xx))) = F(YF)
\end{split}
$$
應用：
$$
\begin{split}
G &:= \lambda \hspace{0.1cm}f\hspace{0.1cm}n.\text{ifz } n \hspace{0.1cm} c_0(\text{add }n (f (\text{pred } n))) \\
\text{sum} &:= YG
\end{split}
$$
# Church-Rosser Property
所以.. 對於任意算式的化簡又或者任意 Jugement 的 Deduction，最終總是會為同一個結果嗎?
考慮這個：
$$(\lambda y.M)((\lambda x.xx)(\lambda x.xx))$$
其中 $M \in \Lambda$ and $y \notin \text{FV}(M)$
要是不斷地做 innermost $\beta$-reduce 將永遠可以操作下去
不過途中如果換成 outermost $\beta$-reduction 會直接收斂至一個**確定**的 normal form
 [^2]
Church-Rosser Property 告訴咱們，任意條求值路徑最終得到的 normal form，一定長得一模一樣
更有趣的，如果一個算式終將能夠收斂至 normal form，那麼用 leftmost outermost evaluation (normal order evaluation) 保證能得到 normal form
而 haskell 在用的 lazy evaluation 就是這個的其中一個 implementation。
# Abstruction
這邊舉幾個常用的函數：
```haskell
length :: [a] -> Int
length [] = 0
length (x:xs) = 1 + length xs
sum :: [Int] -> Int
sum [] = 0
sum (x:xs) = x + sum xs
prod :: [Int] -> Int
prod [] = 1
prod (x:xs) = x * prod xs
maximum :: [Int] -> Int
maximum [] = (minBound::Int)
maximum (x:xs) = max x (maximum xs)
(++) :: [a] -> [a] -> [a]
(++) [] xs = xs
(++) (y:ys) xs = y : (ys ++ xs)
filter :: (a -> Bool) -> [a] -> [a]
filter p [] = []
filter p (x:xs)
| p x = x : (filter p xs)
| otherwise = filter p xs
map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (x:xs) = (f x) : (map f xs)
```
而上述這些程式都能用 foldr 描述出來。
## fold
>程式語言的精隨是什麼？抽象化，抽象化，抽象化！
```haskell
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr f e [] = e
foldr f e (x:xs) = f x (foldr f e xs)
```
粗略的看，foldr 就是這樣的東西：
$$
\text{foldr}\hspace{0.1cm}\otimes \hspace{0.1cm}e \hspace{0.2cm} [1, 2, 3, 4] \cong 1\otimes(2\otimes (3\otimes(4\otimes e)))
$$
不斷地從右邊(r\)做結合(fold)，就是這個 foldr 名稱的由來
在某些語言中，當定義(迭構地[^3])了一個資料結構，就同時附帶一個該資料結構的 fold 能使用
例如自然數 (從 0 開始的)
```haskell
data Nat = 0 | (1+) Nat
foldN :: (a -> a) -> a -> Nat -> a
foldN f e 0 = e
foldN f e ((1+) n) = f (foldN f e n)
```
用 foldN 做加法：
```haskell
(+n) = foldN (1+) n
```
用 foldN 做乘法：
```haskell
(*n) = foldN (n+) 0
```
用 foldN 做偶數判斷
```haskell
even = foldN not True
```
再舉例，資料結構 ITree
```haskell
data ITree a = Null | Node a (ITree a)(ITree a)
```
ITree 的 fold:
```haskell
foldIT :: (a -> b -> b -> b) -> b -> ITree a -> b
foldIT f e Null = e
foldIT f e (Node a t u) = f a (foldIT f e t) (foldIT f e u)
```
## fold-fusion
:::info
TODO: 簡單說明和例子
:::
# Types?
我到現在才知道，以前數學上寫的 function declaration
$$f: \text{ Domain } \to \text{ Codomain }$$
冒號後面就是該 funcition 的 type
> 每個 type 都有自帶一些運算方式
有了 type，可以引導程式設計師去設計出一個正確的演算法
# simply typed $\lambda$-terms (à la Curry)
$$
{\over \Gamma, x:\sigma \vdash x:\sigma}(\text{var})
$$
$$
{\Gamma\vdash M:(\sigma \to \tau )\hspace{1cm} \Gamma\vdash N:\sigma\over \Gamma\vdash MN:\tau }(\text{app})
$$
$$
{\Gamma, x:\sigma \vdash M:\tau\over \Gamma\vdash \lambda x: \sigma .M:(\sigma \to \tau )}(\text{abs})
$$
期末考題：
Derive the typing judgement in simply typed lambda calculus.
$$
\vdash\lambda b.\lambda xy.byx:(\tau\to(\tau\to\tau))\to(\tau\to(\tau\to\tau))
$$
## Well-typed
如果一個 typed lambda term 是 derivable 的，那麼他是 well-typed
## Curry-Howard Correspondence
types 即 propositions, programs 就是 proofs
> 在還沒有機器之前，我們就已經在寫程式了。
柯向上講了一堆很帥的介紹，可惜投影片上沒有，我也記不太清楚，沒辦法重現 QQ
參見 wikipedia: [Curry-Howard Correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence)
> 現在提到咖哩，總是會想到 haskell (
# System F
> 或是 second-order lambda calculus
Terms for System F is defined by:
$$
{M \in \text{ Term}_{\text{Sys F}}\hspace{1cm}t\in \mathbb{V}\over\Lambda t.M\in \text{ Term}_{\text{Sys F}}}(\text{abs})
$$
$$
{M \in \text{ Term}_{\text{Sys F}}\hspace{1cm}\tau\in \mathbb{T}\over(M\hspace{0.1cm}\tau)\in \text{ Term}_{\text{Sys F}}}(\text{app})
$$
其中 $\mathbb{T}$ 就是 types 的 set
哦哦哦！還能跟 type 做 application ㄛ！
這其實就像是：
```haskell
Prelude> maxBound::Int
9223372036854775807
Prelude> maxBound::Char
'\1114111'
Prelude> maxBound::Bool
True
```
在 haskell 看到的型態，其實都隱含一些量詞，例如：
```haskell
a -> a
```
其實表達著：
```haskell
forall a. a -> a
```
也就是說 simply typed lambda term 的規則還能擴充：
$$
{\Gamma, t\vdash M:\sigma\over\Gamma\vdash\Lambda t.M:\forall t.\sigma}(\forall\text{-intro})
$$
$$
{\Gamma\vdash M:\forall v.\sigma\over\Gamma\vdash(M\hspace{0.1cm} \tau):\sigma[v \mapsto\tau]}(\forall\text{-elim})
$$
forall elimination 像是說你可以從一個規模大的 Type 中拿小的 type 出來。
# Functional Programming
Pure function: 不產生 [side effect](https://en.wikipedia.org/wiki/Side_effect_(computer_science)) 的 function
> 不如說 pure function 沒有 implicit states [^4]
side effect:
- 讀/寫 一個變數
- 例外處裡
- IO
- non-determinism
- non-termination
- ...
> 除了 IO 以外，並沒有真正的 Side Effect
pure function 的好：
- 利於重構，畢竟不會改個 function 就動到其他東西
- 方便測試，因為這樣的函數比 impure 的還更容易預測行為
- 能做 function composition
## Monad
> monad 這名字太嚇人了，應該改成 [warm fuzzy thing](https://www.urbandictionary.com/define.php?term=Warm%20Fuzzy%20Thing)
我大概是對 type class 的構造還不太熟悉吧，這裡聽得有點恍神
可以看看阮一峰的： [图解 Monad](http://www.ruanyifeng.com/blog/2015/07/monad.html)
```haskell
class Monad m where
(>>=) :: m a -> (a -> m b) -> m b
return :: a -> m a
```
monad 看起來像是把例外處裡還有函式輸出傳遞到函式輸入的事情包好
> monad 當然也是 pure 的
### monad laws
- left unit: `return x >>= f = fx`
- right unit: `f >>= return = f`
- associativity: `(m >>= f) >>= g = m >>= (\x -> f x >>= g)`
這裡補上 scm 的黑歷史(?)[^5]: [單子 (monad) 入門（一）](https://www.iis.sinica.edu.tw/~scm/ncs/2009/11/a-monad-primer)
# $\pi$-calculus
>其實我真的聽不太懂QQ
$\pi$-calculus 是在 process 上用的模型
它可以用來描述在網路配置上可能隨著計算改變的平行計算
$[\_]$ is asynchronous $\pi$-calculus
_ is synchronous $\pi$-calculus
$[\bar{u}(v).P] = (\nu c)(\bar{u}(c) | c(y).(\bar{y}(v)|[P]))$ where $y \notin \text{FV}(P), c \notin \text{FN}(P)$
$[u(x).P] = u(y).(\nu d)(\bar{y}(d)|d(x).[P])$ where $y \notin \text{FV}(P), d \notin \text{FN}(P)$
## session types
### binary vs multiparty
# 想繼續研究?
在某次教 lambda calculus 課後有朋友推薦我讀這本書： [Understanding Computation](https://www.tenlong.com.tw/products/9781449329273)
嗯.. 封面是某種貝類嗎？感覺很厲害(
然後在~~下飛機~~期末考結束後，咱們一起吃著課程方準備的披薩和炸雞烤雞，隨便聊點什麼(不過邊緣如我，實在不太敢搭話)
陳亮廷對一個想知道怎加入這行的同學說讀看看這兩本： [Basic Category Theory for Computer Scientists](https://www.amazon.com/Category-Computer-Scientists-Foundations-Computing/dp/0262660717)、 [Categories for the Working Mathematician](https://www.amazon.com/Categories-Working-Mathematician-Graduate-Mathematics/dp/0387984038)
柯向上表示 Category theory 有概念是能一句話描述許多邏輯上的事情 (...?) 很厲害的；然後聽說高微裡用的都是 classical logic，必須得忍受排中律 (;ﾟдﾟ)
在 $\lambda$ calculus 課程最後，陳亮廷推了這本： [Types and Programming Languages](https://www.amazon.com/Types-Programming-Languages-MIT-Press/dp/0262162091/)
還有這本： [Lectures on the Curry-Howard Isomorphism](https://www.elsevier.com/books/lectures-on-the-curry-howard-isomorphism/sorensen/978-0-444-52077-7)； 我翻了一下，感覺好難啊.. 但內容很扎實的樣子
據說今年討論程度比以往都還要熱烈啊，我稍微找了以前偶數年的課程內容，啊 沒意外是以前教的太難了然後..
[^1]: [17 年學員的心得文](/k0Cg4mvIQPOkGR6acbnTew?view)
[^2]: [Church–Rosser Made Easy](https://www.cs.cornell.edu/~kozen/Papers/ChurchRosser.pdf)
[^3]: 貌似是柯向上發明的術語，就是 inductively 的意思。
[^4]: [On states](http://joshkos.blogspot.com/2009/05/on-states.html)
[^5]: scm 下課時曾建議我們最好別看他以前的舊文章
Sign in with Wallet
Connect another wallet