duangsuse::Echo

实在是没有那个力气开几个理论向学习，因为定理证明、PL 理论那些已经够累了... 代数程序逻辑依然在学，反正理论向都是均衡发展但都很薄弱就是了

现在具体来讲就是 The Little Schemer 终于熟悉了一点这个列表处理语言... 不过我觉得还是 Haskell 好，因为 Haskell 更符合直觉（看很多用 Haskell 讲程序分析的论文就知道），Scheme 一类的一大堆 car cdr 让不让人活了

具体就是（拿 foldr 和 foldl 举个例子）

Haskell 里（比较简单比较符合那些面向程序分析变换的方式，没有 Foldable、Functor 什么的 class，也是因为我没好好学过 Haskell，羞愧）

foldr :: (a -> r -> r) -> r -> ([a] -> r)
foldl :: (a -> r -> r) -> r -> ([a] -> r)

foldr f v [] = v
foldr f v (x : xs) = f x (foldr f v xs)

foldl f v [] = v
foldl f v (x : xs) = foldl f (f v x) xs

reverse :: [a] -> [a]
reverse = foldl (\xs x -> x : xs) []

map :: (a -> b) -> ([a] -> [b])
map f = foldr (\x xs -> f x : xs) []

length :: [a] -> Int
length = foldr (\_ n -> n + 1) 0

当然，上面的都是 point-free 风格（两边约掉一个参数）（现在你们知道啥叫程序变换了吧？），which 曾经被淫王喷的，因为不直观（实际上他也喷 fold 这种递归模板的，实在是不够直观），不过我是为了讲这个专门举的例子求不喷。

而我们用 Scheme 翻译一下原来简单直观的代码瞬间变成了乱码（这里就没加类型，因为我没试过有静态类型系统的 Scheme 实现）：

(define fold-right
  (lambda (f v l)
    (cond
      ((null? l) v)
      (else (f (car l) (foldr (cdr l)))))))

(define fold-left
  (lambda (f v l)
    (cond
      ((null? l) v)
      (else (foldl f (f v (car l)) (cdr l))))))

(define foldr
  (lambda (f v)
    (lambda (l) (fold-right f v l))))

(define foldl
  (lambda (f v)
    (lambda (l) (fold-left f v l))))

(define reverse
  (foldl
    (lambda (xs x) (cons x xs)) '()))

(define map
  (foldr (lambda (x xs)
    (cons (f x) xs)) '()))

(define length
  (foldr (lambda (_ n)
    (add1 n)) 0))

一　瞬　混　乱
不要停下啊（指乱码）

而且像这种（universality property of fold operator）拿 Scheme 表示就彻底... 彻底（暴论
请善用模式识别。高中生数学科目必须要会的技能

g [] = v
g (x : xs) = f x (g xs)

⇔

g = fold f v

e.g. reverse 函数

reverse [] = [] （其实 reverse [_] 来匹配只有一项的列表也可以，我觉得是这样）
reverse (x : xs) = reverse xs ++ [x]
⇔

reverse = fold f v
  where f = (\x xs -> xs ++ [x])
        v = []

步骤（推算出 f）大概就是 (g xs) 换成 xs...

g (x : xs) =

f x (g xs)
reverse (x : xs) = reverse xs ++ [x]
reverse xs ++ [x] =

((++) (reverse xs) [x])

参数顺序不对，再加层 lambda 表示法就可以了（

定理证明现在勉强理解了一下 rev (rev v) = v 这种，所谓的『更小规模』的证明 forall a v. rev (v ::r a) = a :: rev v 也能勉强理解了，看了证明思路也有，但是还不会写，rewrite 归纳证明比较符合直觉（拿 xs 递归解决什么的...）然后 Agda 总算是看得懂了（我不知道写了多少遍那几个例子才,,,）

28 viewsduangsuse ¯\_(ツ)_/¯ |学渣 ∈ [E²PROM, 含幺半群), edited 10:50