Monads in Category Theory and Monads in Haskell

Aha

最近尝试学习一些基础的范畴论,无奈资质愚钝,浅尝则止了。不过还是想通过这篇文章来加深一下对某些东西的粗浅认识。

我在看monads的定义的时候,总是无法将范畴论中的那套东西联系到haskell中的定义上,为此,我查阅了一些资料,花了很多时间去思考(所谓勤能补拙),总算是让自己相信了。

Monads in Category Theory

从什么地方写起,这是个问题,想了想决定跳过category的定义,直接从functor说起,因为cat的定义比较简单,一搜一看就能理解,而functor在我之前的文章中对它的描述有偏差,这边顺便就纠正了。

Coprime probabilities

A Conclusion

听说了一个有趣的结论:两个随机的正整数互质的概率为 $\frac{6}{\pi ^2}$,对它的推导过程感到好奇,于是通过wikipedia学习了一些数学知识…

Basic Analysis

何为“两个随机正整数”?正整数集合的度是无穷大,所以要使得所有整数对出现的概率相同是无法达到的。

问题需要如此描述:我们用 $Z_2(t)$ 表示互质整数对的个数,其中每个整数对中的两个整数都不大于t,于是所要求的概率即为 $limit_{t \to \infty} \frac{Z_2(t)}{t ^2} $。

我们忽略这个定义,直接考虑无穷的情形,两个整数互质,说明对任意的质数p,它们不能同时被p整除;一个随机正整数被p整除的概率为$1/p$,于是它们不同时被p整除的概率为$1-1/p ^2$,对于不同的质数p,相互独立;于是所求即为:

$$
\prod\limits_{prime\ p} (1-1/p ^2)\tag{1}\label{eq1}
$$.

The Byzantine Generals Problem

闲扯

之前挖下的坑还没有填完,但在此之前,由于各种原因,我决定先写些有关拜占庭将军问题的东西。

拜占庭将军问题是可信计算中的一个非常经典的问题,这个名称我估计是源于Lamport对古罗马的莫名情愫。关于历史的问题,我不懂就不逼逼了。

Problem Description

拜占庭军队有许多分支,驻扎在敌人城外,每一分支由各自的将军指挥。将军们只能靠通讯员进行通讯。在观察了敌人以后,忠诚的将军们必须制订一个统一的行动计划。然而,这些将军中有叛徒。叛徒试图扰乱计划的制定。

因此,能够解决该问题的正确算法必须保证如下两点:

  1. 所有忠诚的将军能够达成相同的行动计划。
  2. 少数的叛徒不能使忠诚的将军做出错误的计划。

The Church-Rosser Theorem

闲扯

最近写的尽是些有的没的,完全没有干货。怎么说,最近考虑在思考人生,价值观在改变,简而言之就是又退化到科学>>技术的中二阶段。一方面看到现阶段所谓“技术产物”的各种各样的问题,另一方面由于自身智力,能力,精力的限制,没有办法对其进行改进和提升,只能采取粗暴的、眼不见为净的鸵鸟政策。其实我知道自己是躲不掉的(当然我说的是找工作),但是还是想在不得不面对之前关心些别的,或者说补救些别的,能补多少是多少吧。年轻的时候有大把时间,却不想念书,现在老了,想念书了,却没有多少时间了(有时间也架不住嗜睡)。

Anyway, 我接下来准备翻译大段的关于无类型lambda-calculus中Church-Rosser定理的证明,为什么要做这么无聊的事情?因为我觉得有趣…为什么不先完善下之前对STLC的证明?1.不求甚解是我的一贯毛(feng)病(ge);2.这个定理在它的证明中会有一丢丢的作用,Normalization证明的补充会在之后进行。

Proof of weak normalization property in STLC

动机

十多天前我在software fundation的练习中过了一遍有关STLC的weak normalization性质的证明
当时有些任务心态,想着把上面留的坑填完就完事了,好多大段的引理证明不仅没仔细看,也没有细想引理的用处。

前几天无意中翻到了王垠的一篇老文,于是试图回忆这个定理的证明过程,却发现脑中是空白的,无奈翻出之前的形式化证明从头屡一屡。

由于我的表述能力的限制,以及我对此证明本质的粗浅认识,这将很难成为一篇好的科普文。另外此文只涉及到关于此性质的核心证明(very informal),其中可能涉及到许多前文已经证明过的引理,如果想了解完整的证明,请参照software fundation或相关文献。

About FLP Proof

Consensus Problem

在分布式系统中,一致性问题的解决是众多分布式算法得以工作的前提条件。这里所说的解决依赖于对系统模型的假设,事实上即便是在工业界得到广泛使用的著名的Paxos算法,也不能完全地解决一致性问题。

Importance

一致性问题是具有普遍意义的。举例来说,一个leader选举算法的safty属性要求算法结束时,所有节点公认某个一致的节点作为其leader;再比如,在一个分布式数据库系统中,某个数据具有多个拷贝,当数据发生变化时,所有这些拷贝都需要做出一致的调整(ACID中的C)。

Auto-fu.zsh customization

大概是这么一回事

放假闲的慌,于是开始折腾些有的没的,忘记是怎么看到这个repo的了…觉得很好玩的样子,就打算试试看。但是折腾的过程中发现,要让这个插件跟我原有的配置共洽,稍稍有点费劲,于是在此记录下我的无聊行径。

选择合适的branch

一开始发现它和zsh-syntax-highlighting闹矛盾,翻了下github的issue,发现有两个branch解决了这个问题,分别是pu和thb,没搞懂名字怎么来的…

pu比thb多了自动纠正,其实我对自动纠正挺反感的,无奈的是thb有些其它的bug,比如在按下tab补全路径的时候会多一个/,总之就是我选择了pu这个分支。

Isomorphisms between Monument Valley & masterpieces of M.C.Escher

Preface

博客写了1.5年左右的时间了,内容尽是些无足轻重的雕虫小技,与其说是博客,不如唤作笔记来的贴切。每当码字的时候,潜意识中总是明白光标下的东西不会被人关注,因此不论是标点、措辞、内容的逻辑性……都全然不顾,敲下的东西更像是当前的我和日后翻阅时的我之间的对话。它们的糟糕程度正好就反映了我的懒散程度。

Vimperator tips 2

Ver 3.8.3 (release) gi触发错误

按键gi的作用是focus到当前页面的input/textarea/iframe,即进入类似vim中的input模式。
在该版本中概率出错(xpath相关,具体记不得了)。
解决办法很简单,安装git版本就可以了。
刚开始看vimperator的源码,尚且不熟悉架构,但是buffer相关的默认按键执行的操作可以在
/common/content/buffer.js中找到。概述信息可以通过mappings module获取,通过
:echo mappings.get(0, 'gi', '.*')

Vimperator tips

vimperator是什么鬼?

对于找到这的人来说,这是个无聊的问题,没办法,好久没写东西了,缺乏基本的文字内容组织能力,
只好遵循渐进的法则…

vimperator 是一个firefox扩展,有很强的可定制性,很好玩,神器,以上。
类似的东西有Pentadactyl(不支持最新的ff),VimFx(功能比较简单)。

好吧,接下来我分享一些vimperator的配置