L. Grayscale Confusion 考虑采用线性函数 f(r, g, b) = x*r + y*g + z*b，对 RGB 的系数和为一且均非负。 可以发现，只有 RGB 各自增 1 才能满足偏序，因此所有满足偏序的颜色对都能被区分开。 对于需要混淆的两个颜色： 如果有 RGB 中的一者相等，假设是 R 相等，直接令系数为 (1, 0, 0)。 如果满足偏序关系，则寄掉。 否则一定存在交错，假设 r_2&preview=true">，，令 , ，那么令： x = q / (p + q) y = p / (p + q) z = 0  就可以实现混淆这两个颜色。 因此可以这样编...

补充：刚刚留意到官方题解提到了这种方式，不过我这里描述稍微详细一点点。 看大家都是用 8 循环，其实还有一种基于对 5 取余的思路： 先考虑 nnn 为 5 的倍数的情况，例如对于 20，我们拆成五组：  1, 6, 11, 16 2, 7, 12, 17 3, 8, 13, 18 4, 9, 14, 19 5, 10, 15, 20  排列内部相减得到 5，只需要排列连接处也能满足题意即可。 尝试把这 5 个排列组合，使之满足题意，变成：  [5, 10, 15, 20], [17, 12, 7, 2], [1, 6, 11, 16], [19, 14, 9, 4], [3, 8, 13, ...

背景 对于本篇文章，你只需要知道将立方类型论理解成一种通过改变形如 A=BA = BA=B 的「相等类型」的构造形式，使得相等类型更能拟合人类直觉（例如过去一些人感觉显然成立的命题，例如函数外延性 (x:A)→f(x)=g(x)→f=g(x : A) \rightarrow f(x) = g(x) \rightarrow f = g(x:A)→f(x)=g(x)→f=g, 不能被证明出来，使用立方类型论就可以轻松证出），且能够证明泛等公理 A≃B→A=BA \simeq B \rightarrow A = BA≃B→A=B. 通常认为立方类型论在软件工程一点用都没有，但在这篇我将尝试给出一些我...

模板是针对高级语言代码生成的一种已有方案之一，工业上的例子包括 ANTLR 等。依值类型被广泛用于证明验证或自动证明，例子包括 Agda 等。然而目前来看模板的自由度极低，应对一些需要展开的任务，例如生成 Golang 代码中的大量错误处理，实现起来比较困难。依值类型虽然允许直接通过搜索生成想要的程序，但其目前在工业界的用例 F* 和 Idris2 都没有和现有语言、现有生态结合的能力，自身没有也难以形成良好的生态。 为综合两方的优势，我提供一种名为 DTmpl 的高级语言代码生成实现思路。DTmpl 取「依值类型」的首字母缩写 DT 和「模板」的缩写 Tmpl 组合而成。不过注意这个是「思路...

上一期博客中我提出了 APTT, 简而言之就是把所有的类型都当作是 x = y 的形式，以提高格式的统一度。但这带来的问题是，进行格式统一后虽然正常的依值类型可以表达，但失去了讨论类型本身的能力。 直观来讲，在 APTT 里面要创建一个类型，往往会得到一个形如 A = refl U 的形式，但我们只能把 A 当作值讨论。不过其实要让 APTT 可以讨论类型也可以，只需要解锁把 A = refl U 这种东西当成值的能力，但这样又会出现不同的继承层级，导致需要不同层级的等号。 路径归纳 APTT 看似带来了可以从路径合并直接推出路径归纳的好处，但实际上在 CuTT 中本来也可以，这可以被转化成从...

最近在学习 CuTT, 虽然没怎么学会，但我在学的时候产生了一个不太一样的类型论构造想法。我的想法是先尝试把我的想法表述出来，这样后续我可能更能理解为什么 CuTT 的一些特定地方采取不同的设计，以及这样会带来什么优势和劣势。 同时我也没有搜索有没有人形成过和我一样的类型论想法，暂时我先当作只有我提出来罢。这大概率是个有很大问题只是我暂时没找到问题的理论（注：我现在大概学会 CuTT 了，确实发现现在这个理论里面有些问题，在下一期博客里面讲一下），小概率这玩意真的有自己的前景。 我将这种类型论构造命名为 All Path Type Theory, 虽然显然不 All Perfect, 但简称 ...

题单里面有 14 道题，要求做至少 10 道。由于我是个大摆子，就挑了 10 道分次做，每次从容易的做到难的。但由于太久没有网瘾，有些难度为「普及-」的题我都需要很久才能产生思路，但也有小蓝题能快速切出来，可能我思路比较清奇。这次主要是记录一些我个人常犯的错误，这样以后印象稍微深刻一些。 P1618 三连击（升级版） 这题其实直接枚举一个数据就行，我枚举了三个，显得非常小丑。当时看算法复杂度对就直接写了，还是需要提高对某种「变量之间的关联」的敏感度，找到求出一系列变量的最简路径。 同时这题被 A=0A=0A=0 的数据搞了一发，我的评价是有点傻呗。理论上对于每一题把每个数据的上下界自己代入一边...

特性声明 本次继续尝试把部分题解放进代码的形式。 题意复述在代码里面，外面只会补充一些细节。 A - GamingForces #include <bits/stdc++.h> #define long long long #define fori(n) for (long i = 0; i < n; i++) #define forj(n) for (long j = 0; j < n; j++) #define rofi(n) for (long i = n - 1; i >= 0; i--) #define rofj(n) for (long j = n -...

官网 写在前面 F* 目前只在 Emacs 有功能全面的编辑器插件， 但可惜本人太菜，只会用 Vim，因此只能在线写码。 State Monad 可以理解为封装后的计算，接受初始状态，返回计算结果和后状态。 let st a = int -> a & int  read 是一个计算，不改变状态，返回的结果是状态本身。 let read : st int = fun s -> s, s  write 是一个计算，忽略原先的状态，接受一个参数 s0 并直接把状态修改成 s0，无计算结果。 let write (s1:int) : st unit = fun _ -> ()...

有人向我反映在代码中写题解会令读者提升血压，我认为这种方式的优缺点如下： 优点  写起来方便，不需要切换界面 便于写一段解释，放一段代码 在代码中也便于顺着上面的注释继续讲解 可以作为写代码的时候使自己思路清晰的一种手段  缺点  非常丑 不支持 LaTeX\LaTeXLATE​X 公式 容易写着写着变成注释的样子  改进方向 理论上如果使用一个更有表达力的语言，便可以基于语言本身生成更多的解释内容，甚至可以生成可以互动的算法演示。我最近在学习的 F* 表达力高于大部分语言，但依然无法达到这种程度。 所以现在呢？ 反正没人看，不如 #include <bits/stdc++.h> ...

P3369 【模板】普通平衡树 #include <bits/stdc++.h> #include <functional> #define ll long long #define fori(n) for (ll i = 0; i < n; i++) #define forj(n) for (ll j = 0; j < n; j++) #define rofi(n) for (ll i = n - 1; i >= 0; i--) #define rofj(n) for (ll j = n - 1; j >= 0; j--) // 本题建议使用平...

链接 官网 内容 讲述了各种数理逻辑符号在 F* 里的原始实现，以及接近数学形式的 squashed form。 提供了 语法糖 来书写用于操作 squashed form 的命题。 个人感觉 F* 提供的语法糖相比 Lean 更冗长，使用体验也比较差，有种 Brainf**k 的感觉 习题一 大意 使用语法糖实现 ~p 的 Introduction 和 Elimination。 AC 代码 let neg_intro #p (f:squash p -> squash False) : squash (~p) = introduce p ==> False with proof_p...

可参考 官网 内容 讲述了不同的等价关系，例如  定义相等  由于采用 Inductive Type 机制，原先表现形式不同的表达式经过自动化简后程序无法区分 例  (fun x -> x) a 和 a (factorial 3) 和 6     证明相等  使用 equal a b 这个类型代表 a == b 的命题 用 Reflexivity x 构造 equal x x 的实例  所有 equal a b 的实例定义相等     布尔相等  仅针对 eqtype，例如 int, bool 等 用 a = b 表示，和非依值类型语言的 a == b 等价    习题一：莱布尼兹等价关...

这些题解是边做题边打的，因此较为省略， 旨在尝试让自己讲明白题目是否能起到贯通思路、减少错误的作用。 A. Everybody Likes Good Arrays! 大意 求最少操作次数使得相邻元素奇偶性不同， 操作为将两个相邻且奇偶性相同的元素合并为乘积。 思路 相同奇偶性乘法不改变奇偶性，所以贪心即可。 维护数据  f / 答案 x, x0 / 新旧读入数字  坑  i = 0 的时候与上一个数字奇偶性相同也不应该加答案！  B. Emordnilap 大意 对每个排列，取其反转后结果拼在后面，求所有情况逆序对数量之和。 思路 数组前后两半逆序对数量之和为 n(n−1)2\frac{n(n...