#dev #tech #English

boot 靴子 引导
stub 存根 占位
review 复习 评审
render 提出 渲染
map 地图 映射
console 安慰 控制台
frame 边框 帧
image 图像 镜像
bus 公交车 总线
access 入口 访问
log 伐木 日志
dump 倾倒 转储
cache 隐藏住所 缓存
port 港口 端口
performance 演出 性能— adolli🍮7️⃣🎏咕嚕靈波（●´∀｀）ノ♡ (@adolli) January 3, 2019

最终没能完成的 #Agda 证明... #Proof 我还是暂时不理解归纳证明

#media #life

是这道证明题

因为我当时没有 Agda 环境而且没看过 Agda 的语法参考，不敢随便修改这些东西，不要以为我只是抄了点代码然后啥都不理解

我好歹还抄了两节课...
我好歹对于 reverse 这种简单递归程序还分析了一会...

不准喷！不准喷！平时你们写那些 Android 应用.... Java 的 Web 后端程序我后来有时间了自然会学...

为了让你们不会喷我只会画个画没前途，特地发我在信息工程方面还会的一些东西...

我真的不是样样通样样松（虽然还并没有样样通）
我真的不是只会画个画，或者只会写个简单的程序或者算法什么的... 真的不是... 别喷

btw. 我这里说的 reverse 是 Haskell 里那种简单的 List reverse

使用 #Haskell 定义如下

reverse' :: [a] -> [a]
reverse' [] = []
reverse' (x : xs) = reverse' xs ++ [x]

当然也可以使用 fold 这种非常具有普适性的 operator 来写，那就是说

foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
reverse'' :: [a] -> [a]
reverse'' = foldr (\x xs -> xs ++ [x]) []

题外话，我以为 infix operator (++) 的类型签名是

(++) :: [a] -> a -> [a]

但其实是

(++) :: [a] -> [a] -> [a]

结果出了很奇怪的类型问题，Couldn't match expected type ‘[a]’ with actual type ‘a’
而我作为 Haskell 初学者居然没有看懂是什么意思，即使人家连是哪里的问题都说出来了（In the second argument of ‘(++)’, namely ‘x’）
我真蠢...

main = do
print $ reverse' [1, 2, 3]
print $ reverse'' [1, 2, 3]

当然，其实你也可以认为 reverse' 和 qsort 类交换排序的函数是很像的

reverse' 的基线条件实际上是列表中只有一个元素的时候，这时候无需交换，递归的话直接返回列表就可以了，至于 reverse [] = []

其实，我们举个例子 reverse' [1, 2] 也即 reverse' 1 : 2 : []

我们来分析一下它的递归定义实际展开处理情况

reverse (x#1 : xs#[2]) = reverse xs ++ [x]
= reverse (2 : []) (1) ++ [1]

where (1)


  = reverse (x#2 : xs#[])
  = reverse ([]) (2)    ++ [2]

where (2)
  = reverse []
  = [] 

其实本来只有一个元素的时候可以不用考虑在 ++ [x] 什么的，直接返回即可（这个递归定义就是这个意思，因为最后一个 case 完全可以不需要再 [] ++ [x]，没必要），像这样
说到这个只是想大家平时多分析点递归定义，和 fold.pdf 那个 papper 上面那样，能由普通的递归函数定义推广到使用 fold 的定义这种能力

reverse'' :: [a] -> [a]
reverse'' xs
| length xs == 1 = xs
| otherwise = reverse'' (tail xs) ++ [head xs]

当然也可以拿 Scheme 写（没有意义，因为是等价的，我只是方便大家熟悉一下 Scheme）：

(define reverse
  (lambda (l)
    (cond
      ((eq? (length l) 1) l)
      (else (append (reverse (cdr l))  (car l))))))

（当然其实不是等价的，Scheme 上不应该 ++ [x] （reverse cons） 而只可以 (cons atom list) 正确的定义
（其实也不是只可以，你可以试试 (append '(1) 2)，不过不是所有标准 Scheme 列表处理函数都支持这种非正规的链表
这样也可以，我们再来看看这个

reverse'' [1, 2, 3]
= [;2] reverse'' [2, 3] ++ [1]

where reverse'' [2, 3]
= [;2] reverse'' [3] ++ [2]

where reverse'' [3]
= [;1] [3]

回溯回来就是 [3] ++ [2] ++ [1] 得 [3, 2, 1]

#Haskell #FP 汉诺塔问题 我说说睡觉算了，尝试独立思考

相传在古印度圣庙中，有一种被称为汉诺塔（Hanoi）的游戏。

该游戏是在一块铜板装置上，有三根杆（编号A、B、C）

在 A 杆自下而上、由大到小按顺序放置 64 个金盘。

游戏的目标：把 A 杆上的金盘全部移到 C 杆上，并仍保持原有顺序叠好。

操作规则：每次只能移动一个盘子，并且在移动过程中三根杆上都始终保持大盘在下，小盘在上，操作过程中盘子可以置于 A、B、C 任一杆上。

问题：现在有 n 个圆盘从小到大叠在 A 柱子上，求如何步数最少的方法把他们移动到 C 柱子上

首先咱有三个 LIFO，模拟这 {A B C} 三根杆子
考虑到时间问题，我不打算找最优解，而且我不认为这周我有能力找什么最优解

Stack A, B, C

*** 我们的盘子大小直接用数字表示，从 1 开始往上数

*** A 是类似这样的：[1, 2, 3, 4, 5, ..., n] （等差数列，差为 1，表示盘子的大小，你也可以认为这是一种 Level）

*** 目标是把 A 上的盘子都移动到 C 杆上，并且保持原有的顺序，就是 [1, 2, 3, 4, 5, ..., n]

规则是每次只能移动一个盘子，移动过程中不得出现 [2, 1] 这种『大盘在上小盘在下』的情况
（原文是 『在移动过程中三根杆上都始终保持大盘在下，小盘在上』）
或者说，不能把大盘子堆在小盘子上面，比如说 A 为 [2, 3] B 为 [1] 则不得 B.moveFrom(A)

所有 Stack 都可以使用以下三种操作
Void moveFrom(self Stack dst, Stack src)，转送一个盘子
Item peek(self Stack stc)，检查栈顶盘子大小
Bool isEmpty(self Stack src)，栈是否为空


为了方便描述，我们建立一个中缀表示法表示 B » A 为 A.moveFrom(B)


咱先来讨论一个简单朴素幼稚一点的小规模问题（直到 A 上有四个元素为止，n <= 4）

首先，假设我们的 A 是 [1]
直接 A » C

然后再 A 是 [1, 2]

如果我们直接 C » A, C » A 两次结果就是 [2, 1]，颠倒了顺序，这样咱怎么办呢？
利用 B 转送。其实就是个简单的大小交换 swap 问题
A » B (B <= 1 =[1])
A » C (C <= 2 =[2])
B » C (C <= B.pop=1 =[1, 2])

或者说

1 « 2 « A
1 » B = 1 « B
2 » C = 2 « C
B » C = 1 « 2 « C

好吧，我们换种方式抽象，尝试使它更直观

A   » B, A » C, B » C
1   » ], 2 » ], 1 » C

我们之所以要利用 B 是因为 C 中数据必须以 1 « 2 « C 的形式存在，2 必须比 1 先压入栈
然而 A 只能出一个 1，它不可能先出 2，所以只好利用 B 去给它缓冲一下（先把 1 存下来）
颠倒压入顺序使得 2 能比 1 先入
A » B (buffer 1)
A » C (cpush 2)
B » C (bputs 1)

然后再 A 是 [1, 2, 3]
因为 A 是 [1, 2, 3]
数据最终肯定还是以 3 » 2 » 1 » C 这种方式压到 C 里面去的
但是它们都是以 1 « 2 « 3 « A 这种方式出来的，需要交换
上面我们其实完成了一次交换，数据流就像这样，好吧上面说过了
不过现在我们其实要考虑 B 里的顺序

A » B, A=[2,3] B=[1] C=[]
A » C, A=[3] B=[1] C=[2]
B » A, A=[1,3] B=[] C=[2]

考虑到上次我们颠倒顺序的经验，可以试试直接套用上次的
1 « 2 如何变成 2 » 1 ？先把 1 » 到 B 上，然后 A(2) 再 » C，然后 B(1) » C，最后 C 是 [1, 2]
这次我们要颠倒的顺序是 1 « 2 « 3，目标是 3 » 2 » 1 » (C)

这里就牵扯到我们的递归了，我们先考虑子问题 1 « 2, which 上面提到过，生成这样的结果

A(1) » B, A(2) » C, B(1) » C
这个『原子性操作』执行完成后 A 为 3 « A, B 为 B, C 为 1 « 2 « C
但这不行啊？显然我们最后要的是 3 » 2 » 1 » C 这个顺序，可是 3 好像不是第一个被压入 C 的，第一个是 2（A » C）

再想想... 首先无需考虑顺序的 buffer 大小，只可能是 1，A 不可能连续两次 » 到 B，实际上 forall s <- {A, B, C}. s » s; s » s 都是不行的，因为那样就颠倒顺序了，否则直接交换算法还很好写的，这是个问题
不过，C 就必须不能被用作『buffer』吗？？？好像未必哦？

** 核心在于『传送中的顺序交换』
1 « 2 « 3 « A 如何弄成 C «r 3 «r 2 «r 1 呢？（»r 是参数反向 cons 的意思，就是把一个元素加到栈顶，不过参数顺序颠倒，皮一下）
A(1) » C
A(2) » B
此时我们的 A=[3] B=[2] C=[1]
我们可以进行的操作是 A«»B A«»C B«»C（反过来也一样），一共 3*3 = 9 种组合
然而考虑到我们的规则（不允许操作后 ABC 中任意一个出现 [x > a, a] 这种序列），实际上能执行的只有 B(2)»A,C(1)»A,C(1)»B
问题解决了吗？没有。我们依然没有办法直接一个操作完成 C «r 3 «r 2 «r 1 这个目标，因为它的前提条件是 C 为 [3]，可现在它是 [1]

显然我们不想让自己的努力白费（选择其他两条等于撤销自己之前的『分布』操作），只好选择 C(1)»B 这条路
完成后栈们是这个样子的： A=[3] B=[1,2] C=[]
看到了吗？A=[3]，而 C=[]，这意味着我们可以用 A » C 来完成我们之前定下的 C «r 3 顺序的第一步了！感谢我们之前执行的 A » B; A » C; C » B 操作！

这一次执行的是 A » C; A » B; C » B
这个操作之前栈们是这样的： 1 « 2 « 3 « A, B, C

1. 2 « 3 « A, B, 1 « C
2. 3 « A, 2 « B, 1 « C
3. 3 « A, 1 « 2 « B, C

而其实我们最终期望的是能够完成 C »r 3 »r 2 »r 1 这个任务，但显然只有 C 为空栈，一个栈上可以弹出 3 的时候才可能完成

+ A=[1,2,3] 这时不可能完成，所以我们试着移动数据到 B (a)
+ A=[2,3] B=[1] 这时依然不可能完成，所以尝试移动到 C (b)
+ A=[3] B=[1] C=[2] 这时我们看到了 A 上可以弹出 3 了，但是 C 不为空栈

为什么和我们开始的选择不一样？为什么这个就『不行』？

而上面的操作 (a) 和 (b) 的顺序其实 matters，因为这关系到 1 和 2 最终分别归 C 还是 B，我们可以从中汲取灵感
+ 如果先出队给 C，则最后 C=[1] B=[2] （就是『可以』的情况）
+ 否则，出队给 B，则最后 B=[1] C=[2] （就是那个『不可以』的 case）

从中我们可以分析得知，
出队给 C，也即出队『小』元素给『最终』的 vector 才是可行的
这样之后才可以 C（包含小元素） » B（包含大元素），不然 B=[1] C=[2] 这个 case，不能进行 C » B 操作，使得 C 变成空栈


之后是这样的：3 « A, 2 « B, 1 « C

上一次做的则是 A » B; B » C; A » C
这个操作之前栈们是这样的： 1 « 2 « A, B, C
之后是这样的：A, B, 1 « 2 « C
看出什么规律来了吗？？？

接下来即得易见平凡，A » C 之后 A=[] B =[1,2] C=[3]
又回到了之前的问题，之前的问题是 A=[1,2] 时怎么转送到 C，我们实际上只要求 B 柱顺序了
B(1) » A; 此时我们可以操作的组合又多出来不少，然后我们选择一个能做下一步 C «r 2 的
B(2) » C; 此时 A=[1] B=[] C=[3]
最后 A » C，问题完成了！

然后是可能和基线问题无关的一个额外的呃... 推广？？？好像不是，反正就是另外举个例子加深理解

A=[1,2,3,4]

（此处留给读者时间独自完成题解）

答案很明显。
套用操作序列 A(smaller) » C; A » B(bigger); C(smaller) » B(bigger)
结果是 A(1) » ]C; A(2) » ]B; C(1) » B，最终 A=[3,4] B=[1,2] C=[]

我们发现一个尴尬的状况 — 此时 C «r 4 所需要的情况（C 为空栈，一个栈可以弹出 4）不成立
不过机制的你肯定也发现了，C 此时是空栈呢！这说明我们可以做一些好玩的事情

A » C; B » C，完成后 A=[4], B=[2], C=[1, 3] 我们发现 C » A 可以完成一次交换 A=[1,4] B=[2] C=[3]...
{NEXT}

rt. 其实就这个可能不是最优解的解法也没有什么太大的难度，不过这个的确是比较好玩的，因为题目看起来令人无法理解。

总之呢... 独立从 '0' 解决这种问题真的是很困难的，但是，说实话，不能归纳出最基本的特征，就无法实际的独立完成归纳证明，而证明为什么 "foo".reverse().reverse ≣ "foo" 的能力是我所缺失的

希望大家多少从咱这里学了点问题分析方法的说
做起来真的是相当 Excited 🐸👍
我说完了。

where {NEXT} is:

好吧，貌似不好玩，那找找原因

第一次 input 是 A=[1,2]


A(s)»B
A(b)»C
B(s)»C

交换的顺序是 1,2 -> 2,1
我们做的是先把 s 放在缓冲栈里，然后把 b 放到目标里，然后把 s 里的缓冲压入目标栈
这就是一次交换，归纳出来就是 src(smaller) » buf; src(bigger) » dst; buf(smaller) » dst

第二次 input 是 A=[1,2,3]
我们不得不再多考虑一个缓冲的顺序，也即更大意义上的顺序
因为缓冲是有限的，所以得弄出一套全新的理论解决这个问题
A(s) » C ; C=[] -> C=[1]
A(b) » B ; B=[] -> B=[2]
C(s) » B ; [1] » [2]

交换完出现一个非常令人 excited 🐸 的情况，C 直接为空栈了，而此时最大的 3 也被暴露在 A 栈顶了，我们可以开始实际解决问题了

A » C ; C=[3]

再做一次交换，因为此时 B 依然是顺序的，我们套用之前的 routine

def naive-swap(dst, buf, src) = src(smaller) » buf; src(bigger) » dst; buf(smaller) » dst

这里，我们定义（其实本质上是对问题的归纳）了一个函数，称它为 naive-swap，它需要输入三个参数

dst：汉诺塔 LIFO
src：至少有两个元素的汉诺塔 LIFO
buf：一个不存在大小比较问题的汉诺塔

它产生副作用，将 src（如 [1,2]）以反向压入到 dst 中（如最后 dst=[2,1]）
它还有一个要求要点，就是 src 的栈顶元素必须比 buf 的栈顶元素小，不然不能进行移动
对于 dst 也一样，src 栈顶后的下一个元素（比如 2）必须比 dst 的栈顶元素（正例，比如 3）小，不然也不能进行移动
（这些约束都是为了符合汉诺塔的定义，当然本来就有这些约束不过我特别指明这些）

上面那个 A » C; A » B; C » B
where A=[1,2,3]
我们其实也可以注意到了，它其实就是 naive-swap(A,C,B)

naive-swap(A,C,B) where A=[1,2,3] B=[] C=[] 的结果就是 A=[3] B=[1,2] C=[]

之后在这个结果上，我通过枚举组合和猜测的方式（<del>费曼算法</del>）得出了解法 A(3) » C; B(1) » A; B(2) » C; A(1) » C

其实，它也可以被归纳为使用 naive-swap 的版本，利用子程序可以使我们更好的抽象问题：

A » C; naive-swap(B, A, C)

其实，我们注意到，naive-swap 就是这个递归问题的『最本质，最小规模的子问题』

A=[] 时，无需任何操作
A=[1] 时，简单的 A » C 即可
A=[1,2] 时，执行 naive-swap(A,B,C)
A=[1,2,3] 时，执行 naive-swap(A, C, B); A » C; naive-swap(B, A, C)

我们来猜测一下，A=[1,2,3,4] 时该怎么样？

A=[1,2,3] 时
naive-swap(A, C, B) 后
A=[3], B=[1,2], C=[]

然后我们把『暴露』在 A 栈顶的 max value 送到 C 中（A » C）
最后从 B[1,2] 移动到 C[3]（naive-swap(B, A, C)），问题解决

...我好歹还是猜了一下...

A=[1,2,3] 时，首先处理 A=[2,3]
naive-swap(A, C, B)
A=[3], B=[1,2], C=[]
然后 A=[1]，A » C
naive-swap(B, A, C)

A=[1,2,3,4] 的时候，首先处理 A=[2,3,4]：

naive-swap(A, B, C)
[3,4] [] [1,2]

A » B
[4] [3] [1,2]

naive-swap(C,B,A)
[4] [1,2,3] []

A » C
** [] [1,2,3] [4]

终于，在我的一番胡乱猜测之后，回到了基线问题
至于『为什么』，我懒得追究了，来看看递归思路吧。

naive-swap(A,B,C);A»B;naive-swap(C,B,A);A»C 之后，A=[1,2,3,4] 变成了 A=[] B=[1,2,3] C=[4]

我们成功的让 A=[1,2,3,4] 变成了 A=[1,2,3] ！！！这是个大突破。

怎么办呢？我们定义

def naive-swap(dst, buf, src) = src(smaller) » buf; src(bigger) » dst; buf(smaller) » dst

def a123(SubA, SubB, SubC) = naive-swap(SubA, SubC, SubB); SubA » SubC; naive-swap(SubB, SubA, SubC)

这里，我们所谓的 『A』 是 B，『B』是 A，『C』依然是 C

然后我们调用 a123(B, A, C) 即可完成交换

（这里留点时间大家自己推导一下 A=[1,2,3,4,5] 的情况）

综上所述 #Learn #Haskell #FP #Algorithm

汉诺塔问题，问题的定义在这里 我对问题的抽象在这里

尝试使用递归算法求得可行解

我之前通过一̶长̶串̶失̶败̶的̶尝̶试̶总结出了规律

def naive-swap(dst, buf, src) = src(smaller) » buf; src(bigger) » dst; buf(smaller) » dst

这是一个较小规模的子问题

可以得知
+ A=[] 时无需进行任何操作
+ A=[1] 时进行 A » C
+ A=[1,2] 时直接 naive-swap(A, B, C)
+ A=[1,2,3] 时

  naive-swap(A, C, B)

[3] [1,2] []

  A » C

[] [1,2] [3]

  naive-swap(B, A, C)

[] [] [1,2,3]
+ A=[1,2,3,4] 时

  naive-swap(A, B, C)

[3,4] [] [1,2]

  A » B

[4] [3] [1,2]

  naive-swap(C, A, B)

[4] [1,2,3] []

  A » C

[] [1,2,3] [4]

我们可以依此推导出 A=[1,2,3,4,5] 时的数据转移情况
... 算了，因为今天有点晚了

See Also:
+ 各种语言的算法实现

+ 某博客的教程

+ Haskell 图解，并且使用了 Haskell 可视化包

+ 一个延伸的汉诺塔问题

+ Wikipedia Hanoi
+ Wikipedia 递归

== Haskell 的副作用版解法

hanoni n (a, b, c)
| n == 1 = putStr (a ++ "->" ++ c) >> putStrLn ";"
| otherwise
= do
hanoni (n - 1) (a, c, b)
hanoni 1 (a, b, c)
hanoni (n - 1) (b, a, c)

main = hanoni 5 ("A", "B", "C")


解法的基本思想是递归。假设有 A、B、C 三个塔，A 塔有 N 块盘，目标是把这些盘全部移到 C 塔。那么先把 A 塔顶部的 N − 1 块盘移动到 B 塔，再把 A 塔剩下的大盘移到 C，最后把 B 塔的 N − 1 块盘移到 C

A=[1,2]
[2] [1] []
[] [1] [2]
[] [] [1,2]

A=[1,2,3]
... (naive-swap(A,C,B))
[3] [1,2] []
[] [1,2] [3]
... (naive-swap(B,A,C))
[] [] [1,2,3]

A=[1,2,3,4]
...
[4] [1,2,3] []
[] [1,2,3] [4]
[] [] [1,2,3,4]

A=[1,2,3,4,5]

[5] [1,2,3,4] []
[] [1,2,3,4] [5]
[] [] [1,2,3,4,5]

......