9032676's Blog

前阵子正看着 HoTT Book 中 1.12 节，即讲述 identity type 与 path induction 之类的概念，透过 Agda 对其研究与学习之后决定写一篇文章记录下有关这些概念的一些理解，以巩固一下自己对这些概念的认识。 引言 在 Agda 中，我们或多或少在一些需要证明命题等价性的 module 中可能会看到 {-# OPTIONS --without-K #-} ... 続きを読む…

引言 由于最近打算多学一点抽象代数的知识，鉴于之前已有范畴论方面的铺垫，并且希望透过范畴论的方式来学习抽象代数，因此采用了 Algebra: Chapter 0 - PaoloAluffi 这本书来作为我的自学参考书。本篇内容将从第二章 开始（跳过基础的集合论与范畴论介绍），并以随手的方式速记。 Chapter II - Groups, first encounter 1. Definiti... 続きを読む…

阅读须知 本篇文章面向人群是接触过 Category theory (范畴论) 以及 函数式编程，但未曾接触过 Yoneda Lemma (米田引理) 的读者食用。 通篇对于范畴论内的专有名词一律采用了英文词汇的形式表达，以防中文翻译各类型文章不统一，可能存在误导性。 文章中可能会存在一些 Agda 或 Haskell 语言的代码。没有相关知识不要紧，这只是给予相关领域的朋友一个直觉，用以... 続きを読む…

简介 最近由于正在研究直觉类型论以及同伦类型论, 因此特意挑选了 Scala 的 Dotty 编译器作为研究对象, 而由于 Dotty 所设计的依赖类型相较于 Coq, Agda, Idris 之类的语言来讲十分不直观, 导致写出一些带有大量依赖类型的函数则显得较为绕口, 因此本篇文章主要目的是找出一套通用的编码方式, 亦即找寻出 Scala 与 直觉类型论 之间的对应关系. 在 Dotty... 続きを読む…

简介 于 直觉类型论 (Intuitionistic type theory, 或 Martin-Löf's type theory) 中, 定义了一些于经典类型论中没有的高阶类型: \(\Pi\)-类型 (依赖函数类型, Dependent function types) 以及 \(\Sigma\)-类型 (依赖乘积类型, Dependent pair types), 该种类型系统可被对应... 続きを読む…

简介 于理论计算机科学中, Church-Rosser 定理 讲述了当我们尝试给任意 \(\lambda\)-表达式 的变体应用 \(reduction\) 规则时, 不管所规约排序如何, 也定不会影响到最终的运行结果. 该定理由 Alonzo Church 与 J. Barkley Rosser 于 1936 年时证明得出, 并以他们的名称所命名. \(\beta\)-范式 (\(\bet... 続きを読む…

続きを読む…

简介 不动点组合子 (Fixed-Point Combinator) 是一种计算其他函数 不动点 (Fixed-Point) 的高阶函数. 有函数 \(f\) 其输入值 \(x\) 若与返回值相同 (同样是返回 \(x\), 即 \(f(x) = x\)), 则称之为函数 \(f\) 上的不动点为 \(x\). 例如现在有 \(f(x) = x ^ 2\), 则其不动点是 \(f(0) = ... 続きを読む…

简介 在数学 (尤其指数理逻辑分支) 与类型论的世界, Lambda 立方体 是由 Henk Barendregt 提出的一个框架, 用以探索及研究 简单类型 \(\lambda\)-演算 于不同维度上扩展出来对应的 类型系统, 其也阐述了处于不同维度上的 类型系统 中 类型 (Type) 与值 (Term) 的依赖关系 究竟是怎样的, 简单来说我们可以以三种不同方向的箭头 (维度) 定义出... 続きを読む…

前言 上一章介绍了除集合范畴以外一些其他范畴的例子，而对于任意范畴而言，往往是由态射把不同对象链接在一起形成某些关系。而既然我们已经知道了一些不同种类态射与范畴，当然对象也不会例外，透过对对象种类的划分，我们同样地可以得出一些不同的结论出来，因此我们今天就来探讨下关于范畴内对象的一些关系吧。 泛构造（Universal Construction） 在范畴论的语言中，我们常常都会把对象之间透过... 続きを読む…