排版测试

module TypesettingTests where

这是一个排版测试,用来检验 Jekyll 、 MathJax 和 Liquid 的功能能否在我的 Literate Agda 博客中正常运作。

Jekyll

module Jekyll where

好像没什么功能……

MathJax

module MathJax where

  postulate SimpleDefinitions : Set

以下内容盗取自这里

\(\lambda\)-算子

早在上世纪 30 年代, 理论上早已出现了许多种不能跑在当下计算机中的 “编程语言”, 甚至编程语言这个概念还尚未成熟, 当时人们主要研究 formal system (形式系统) 这一领域. 而这其中最为突出的成果为图灵的导师 Alonzo Church 的 \(\lambda\)-算子, 它是 FP 中非常重要的理论基石, 之后的文章也都全部围绕这一系统进行讨论.

在讨论 \(\lambda\) 表达式之前, 我们需要一个 context (上下文), 它类似于我们所说的集合论中的 universe 集合 (全集) \(U\), 它保证了我们的论域中拥有独一无二的元素, 写作 \(\Gamma\). \(\Gamma\) 可以是一个空集 \(\varnothing\), 也可以是引入了某元素后的集合, 以此类推. 类比一般的高级编程语言, 它就像符号表, 像一个装有独特变量的相关信息的 哈希表, 甚至也可以是放有变量名的 (数据结构里的) 集合, 当然这些只是比喻.

我们定义一个 \(\lambda\) 函数, 在 \(\Gamma\) 下引入, 形为

\[\Gamma \vdash \lambda x . x\]

它类似数学中常用的函数 \(f(x) = x\), 但这种表示引入了函数名称 \(f\), 而 \(\lambda\) 函数是 匿名 的, 两者显然并不等同. 这种最基本的 输入即输出 的函数, 被称作 identity function.

和数学中常用的函数表示更加不同的是, 一个 \(\lambda\) 函数可以返回另一个 \(\lambda\) 函数, 而且对上一个函数的参数是可见的, 即以下函数表示是合法的

\[\lambda x . \lambda y . x\]

简记为

\[\lambda x y . x\]

这一种特性叫做 lexical scoping. 有了这一种特性, 我们便可以做到多参数输入, 单结果输出了. 那具体是怎么做的呢? 首先我们先看一个简单的场景

\[\Gamma \vdash (\lambda x . x) (\lambda y . y)\]

这句话的意思是, 给定一个 context 叫 \(\Gamma\), 我们将两个 \(\lambda\) 函数添加到 \(\Gamma\) 之中. 接着我们用第一个函数的参数 \(x\) 代替第二个函数的整体, 按照第一个函数的 “执行规则”, 返回一个新的 term (), 即

\[(\lambda x . x) (\lambda y . y) = _\beta \lambda y . y\]

这一句话的 “执行结果”, 即第二个函数本身. 前面将函数加入到 context 中的过程, 我们简称 eval (即 evaluate), 而实际执行这些函数的过程, 简称 apply, 而之前所提到的 “执行规则”, 称作 \(\beta\)-reduction, 它属于一种 term rewriting rules (项的重写规则). 可见, 在 \(\lambda\)-算子 这个系统中, 最基本的操作即 eval/apply 两个过程的循环.

至于刚刚提到的 多参数输入, 单结果输出, 考虑以下的例子

\[\Gamma \vdash (\lambda xy.x) (\lambda a.a) (\lambda b.b)\]

其 apply 的过程即

\[ (\lambda xy.x) (\lambda a.a) (\lambda b.b) \equiv (\lambda x.\lambda y.x) (\lambda a.a) (\lambda b.b) \\\\ = _\beta (\lambda y.(\lambda a.a)) (\lambda b.b) \\\\ = _\beta \lambda a.a \]

  postulate InlineLaTeX : Set

我觉得这 \(\uparrow\) 很重要。

Agda 代码

postulate
  blah : Set
  bbb  : blah
record A (B : Set) : Set where
  field map : B
ins : A blah
A.map ins = bbb
_ = map where open A ins -- without qname
_ = M.map where module M = A ins -- qname