5eqn
5eqn
全部文章
分类
PLT(11)
题解(12)
归档
标签
去牛客网
登录
/
注册
Blog of 5eqn
算竞边缘人的奇思妙想
全部文章
(共23篇)
题解 | #Agnej#
D. Agnej 博弈,m 为偶数的时候最后一定是变成每层两半各留一个,直接统计 1 的数目判断奇偶性; m 为奇数的时候先默认大家都会薅掉中间的,这样还是每层两半各留一个。但是只要某层某一半没了,中间还在,中间就不能被薅掉了。 假设某一层中间被包裹得很好,例如 1 1 1 1 1,至少需要薅掉两个...
2023-08-18
1
582
题解 | #Grayscale Confusion#
L. Grayscale Confusion 考虑采用线性函数 f(r, g, b) = x*r + y*g + z*b,对 RGB 的系数和为一且均非负。 可以发现,只有 RGB 各自增 1 才能满足偏序,因此所有满足偏序的颜色对都能被区分开。 对于需要混淆的两个颜色: 如果有 RGB 中的一者相...
C++
2023-08-18
2
921
题解 | J. Permutation and Primes
补充:刚刚留意到官方题解提到了这种方式,不过我这里描述稍微详细一点点。 看大家都是用 8 循环,其实还有一种基于对 5 取余的思路: 先考虑 nnn 为 5 的倍数的情况,例如对于 20,我们拆成五组: 1, 6, 11, 16 2, 7, 12, 17 3, 8, 13, 18 4, 9, 14...
C++
2023-08-11
2
444
立方类型论在软件工程中的用例设想
背景 对于本篇文章,你只需要知道将立方类型论理解成一种通过改变形如 A=BA = BA=B 的「相等类型」的构造形式,使得相等类型更能拟合人类直觉(例如过去一些人感觉显然成立的命题,例如函数外延性 (x:A)→f(x)=g(x)→f=g(x : A) \rightarrow f(x) = g(x) ...
CuTT
Idris2
2023-07-17
1
653
DTmpl: 基于依值类型和模板的高级语言代码生成思路
模板是针对高级语言代码生成的一种已有方案之一,工业上的例子包括 ANTLR 等。依值类型被广泛用于证明验证或自动证明,例子包括 Agda 等。然而目前来看模板的自由度极低,应对一些需要展开的任务,例如生成 Golang 代码中的大量错误处理,实现起来比较困难。依值类型虽然允许直接通过搜索生成想要的程...
Idris2
Go
2023-07-15
0
317
对上一篇提出的类型论的探讨
上一期博客中我提出了 APTT, 简而言之就是把所有的类型都当作是 x = y 的形式,以提高格式的统一度。但这带来的问题是,进行格式统一后虽然正常的依值类型可以表达,但失去了讨论类型本身的能力。 直观来讲,在 APTT 里面要创建一个类型,往往会得到一个形如 A = refl U 的形式,但我们只...
Idris2
CuTT
2023-07-13
0
414
一个抽象的类型论想法
最近在学习 CuTT, 虽然没怎么学会,但我在学的时候产生了一个不太一样的类型论构造想法。我的想法是先尝试把我的想法表述出来,这样后续我可能更能理解为什么 CuTT 的一些特定地方采取不同的设计,以及这样会带来什么优势和劣势。 同时我也没有搜索有没有人形成过和我一样的类型论想法,暂时我先当作只有我提...
Idris2
CuTT
2023-07-11
0
376
HITsz 第一周题单浅评 模拟枚举暴力
题单里面有 14 道题,要求做至少 10 道。由于我是个大摆子,就挑了 10 道分次做,每次从容易的做到难的。但由于太久没有网瘾,有些难度为「普及-」的题我都需要很久才能产生思路,但也有小蓝题能快速切出来,可能我思路比较清奇。这次主要是记录一些我个人常犯的错误,这样以后印象稍微深刻一些。 P1618...
C++
2023-07-09
1
475
Educational Codeforces Round 142 思路 + 代码 A, B, C, D
特性声明 本次继续尝试把部分题解放进代码的形式。 题意复述在代码里面,外面只会补充一些细节。 A - GamingForces #include <bits/stdc++.h> #define long long long #define fori(n) for (long i = 0;...
C++
2023-01-25
0
1118
FStar 官方习题 A First Model of Computational Effects
官网 写在前面 F* 目前只在 Emacs 有功能全面的编辑器插件, 但可惜本人太菜,只会用 Vim,因此只能在线写码。 State Monad 可以理解为封装后的计算,接受初始状态,返回计算结果和后状态。 let st a = int -> a & int read 是一个计算,不...
F*
2023-01-23
2
323
首页
上一页
1
2
3
下一页
末页