11个版本
| 0.0.10 | 2023年8月27日 |
|---|---|
| 0.0.9 | 2023年3月18日 |
| 0.0.3 | 2023年2月28日 |
#935 in 算法
每月27次下载
285KB
4.5K SLoC
类型
- 可判定的（或仅是完整的？）
- 有序/非交换的
- 线性/非确定性的（⊇ 正则/确定的）
- 无单位的/促同调的
待办事项
- 是否存在这样的选择/投射乘法，只连接And的一侧？
- 四个单位的表示，或者我们需要它们？（可判定的受到影响）
- 1作为Seq::empty()，𝟏 ≡ νX.X
- 𝟎 ≡ μX.X
- ⊤作为Inf(Interval::full())
- ⊥作为a ≠ b时的a & b (?A)
- One作为Seq(['a'])与Interval('a', 'a')
- 名义性、输入/字符串与函数参数/抽象、积分特性和De Bruijn索引之间的关系
- TextStart和TextEnd作为左/右单位
- 对
match的解释，它是一个判断a : A还是一个测试一个是否能被另一个整除（商等于零）a / b，一个（字符串）被另一个（正则表达式）包含a → b？证明搜索 - 对于每个正连接词有两种否定类型：Seq的rev和div，Interval的not和sub
- a.le(b) → a.and(b) = a，a.add(b) = b
- 等价推理，模拟
- 归纳
- True(Seq<I>, Box<Repr<I>>)，断言，依赖类型，回引用
- 动作a.P，a ⊙ P，守卫，标量积
- 范式与等价规则
- 特征函数/态射
- 加权极限，加权余极限，端，余端
- 将某些法则作为特性参数化
- 球面圆锥（网球）
映射
- 分组和捕获的功能等价
异或
- 前瞻/后顾，多个未来，通信和丢弃，
ignore组合子 - 分割，子空间
比较
| 正则表达式/ 集合论 |
线性逻辑 | repr | 类型论/ 范畴论 |
len | 进程演算 | 概率论/ 学习理论 |
量子理论 |
|---|---|---|---|---|---|---|---|
| a ∈ L (match) | a : A (判断) | ||||||
| $∅$ | $0$ | nil，STOP | |||||
| $⊤$ | True | ||||||
| a | a | One(Seq(a)) | len(a) | (顺序组合，前缀) | |||
| $ε$ (空) ∈ {ε} | $1$ | Seq([]) | * : 1 | 0 | SKIP | ||
| . | Interval(MIN, MAX) | 1 | |||||
| ab / $a · b$ (连接) | $a ⊗ b$ (乘法连接/乘法) | Mul(a, b) | $a ⊗ b$ (张量积) | len(a) + len(b) | P ||| Q (交错) | ||
| a|b (交替), $a ∪ b$ (并集) |
$a ⊕ b$ (加法析取/加号) | Or(a, b) | $a + b$ (余积) | max(len(a), len(b)) | (确定性选择) | ||
| a* (Kleene星), ..|aa|a|ε |
$!a$ (指数合取/当然) νX.1 & a & (X ⊗ X) |
Inf(a) | ν, 不动点/迹，共モナード，最终煤代数 | (复制) | |||
| a*? (非贪婪), ε|a|aa|.. |
$?a$ (指数析取/为什么不) $µX.⊥ ⊕ a ⊕ (X ⅋ X)$ |
Sup(a) | μ, モナード，初期代数 | ||||
| a? | a + 1 | Or(Zero, a) | |||||
| a{n,m} (重复) | a | Or(Mul(a, Mul(a, ..)), Or(..)) | |||||
| [a-z] (类) | Interval(a, z) | ||||||
[^a-z] (否定) |
TODO 这是对称操作 | Neg(a)/-a |
|||||
| a† (反转) | 右律 vs 左律 | a.rev() | len(a) | ||||
| $a / b$ (右商) | $a ⊸ b$ | Div(a, b) | len(a) - len(b) | (隐藏) | |||
| a \ b (左商) | Div(a,b) |
(隐藏) | |||||
| RegexSet | a ⅋ b (乘法析取/并) | Add(a, b) | $a ⊕ b$ (直和) | (非确定性选择) | |||
| $a ∩ b$ (交集) | a & b (加法合取/与) | And(a, b) | $a × b$ (积) | (接口并行) | |||
a(?=b) (正向先行断言) |
And(a, b) | ||||||
a(?!b) (负向先行断言) |
And(a, Not(b)) | ||||||
(?<=a)b (正向后行断言) |
And(a, b) | ||||||
(?<!a)b (负向后行断言) |
And(a, b) | ||||||
| $a ⊆ b, a ≤ b$ (包含) | $a ≤ b (≃ a = b ⅋ a < b)$ | a.le(b) | |||||
| a⊥ (对偶) | a.dual() | ||||||
| a = b (等价) | a = b (恒等型) |
关于符号
符号根据加法/乘法区分分组和分配。它们对应于计算是否存在或继续；尽管连接 ⊗/Mul/* 有连接意义，计算不会在满足一个标准时不完成/退出，因为还有不同的分区方式尝试（回溯）。尽管 RegexSet ⅋/Add/+ 有析取意义，计算不会在满足一个标准时返回哪个正则表达式匹配。另一方面，交替 ⊕/Or/| 和交集 &/And/& 早期断言，因此有顺序依赖性。当我将 Map 变体添加到 Repr 以执行任意函数时，这种顺序依赖性突然变得很重要，因为这些任意函数可以有影响，例如，输入字符串的修改/替换。 (影响是可加的。)
| 加法 | 乘法 | 指数 | |
|---|---|---|---|
| 正/外延 | $⊕$ $0$ Or | $⊗$ $1$ Mul | ! |
| 负/内延 | & ⊤ And | ⅋ ⊥ Add | ? |
律/一致性
- 所有连接词都是结合的
- 加法连接词是交换的且幂等的
待办事项
- Seq::empty(), ε - 可以是空的，因为负
- Interval::full() - 不能为空，因为它是正的
| 正则表达式 | 线性逻辑/量子集 | repr | 标题 |
|---|---|---|---|
| $a | (b | c) = (a | b) | c$ | $a ⊕ (b ⊕ c) = (a ⊕ b) ⊕ c$ | Or(a, Or(b, c)) = Or(Or(a, b), c) | Or-结合律 |
| a | a = a | $a ⊕ a = a$ | Or(a, a) = a | Or-幂等律 |
| $a ⊕ 0 = 0 ⊕ a = a$ | Or(a, Zero) = Or(Zero, a) = a | Zero, Or-单位 | |
| $a · ε = ε · a = a$ | $a ⊗ 1 = 1 ⊗ a = a$ | Mul(a, One('')) = Mul(One(''), a) = a | One(''), Mul-单位 |
| $a · (b | c)$ | $a ⊗ (b ⊕ c) = (a ⊗ b) ⊕ (a ⊗ c)$ | Mul(a, Or(b, c)) = Or(Mul(a, b), Mul(a, c)) | 右分配律 |
| $(a ⊕ b) ⊗ c = (a ⊗ c) ⊕ (b ⊗ c)$ | Mul(Or(a, b), c) = Or(Mul(a, c), Mul(b, c)) | 左分配律 | |
| $ε^† = ε$ | |||
| (a & b)† = (b†) & (a†) | Rev(Mul(a, b)) = Mul(Rev(b), Rev(a)) | ||
| Mul(One(a), One(b)) = One(ab) | |||
| a ⅋ (b & c) = (a ⅋ b) & (a ⅋ c) | Add(a, And(b, c)) = And(Add(a, b), Add(a, c)) | 右分配律 | |
| (a & b) ⅋ c = (a ⅋ c) & (b ⅋ c) | Add(And(a, b), c) = And(Add(a, c), Add(b, c)) | 左分配律 | |
| a & a = a | And(a, a) = a | And-幂等律 |
加法、乘法和指数之间的关系
- exp(a + b) = exp(a) * exp(b)
线性（哪个）
- f(a + b) = f(a) + f(b)
- (a → b) + (b → a) (非构造性）
- 函数只接受一个参数
- 模块的预层
𝜕, 导数
| 数学 | repr |
|---|---|
| $𝜕(a ⊗ b) ≃ 𝜕(a) ⊗ b + a ⊗ 𝜕(b)$ | der(Mul(a, b)) = Or(Mul(der(a), b), Mul(a, d(b))) |
- d(Zero) = Zero
- d(Or(a, b)) = Or(d(a), d(b))
- d(Mul(a, b)) = Or(Mul(d(a), b), Mul(a, d(b)) *)
- d(Inf(a)) = Mul(d(a), Inf(a))
- a : D(a)
True
- And(True, a) ->
流处理器
- νX.μY. (A → Y) + B × X + 1
标志（待办事项）
-
i，不区分大小写 -
m，多行 -
s，点匹配新行 -
U，交换贪婪 -
u，Unicode -
x，忽略空白 -
使用非贪婪模式将_替换
解释
- 将匹配视为将字符串出现分配给表达式的每个部分的过程，正则表达式是资源（字符串出现的有限次数）消耗（它们之间的独占分配/匹配）。
不要说“通信”
- 局部 ↔ 全局
- 相互提供/解决/适应上下文
算法（待办事项）
- 位并行
- aho-corasick
- Boyer–Moore
- memchr
语义（待办事项）
- 一致空间
参考
- 广义自动机类别的完备性，Guido Boccali，Andrea Laretto，Fosco Loregian，Stefano Luneia，2023 [arxiv]
- 超越初始代数和最终合代数，Ezra Schoen，Jade Master，Clemens Kupke，2023 [arxiv]
- 功能机器演算，Willem Heijltjes，2023 [arxiv]
- 功能机器演算II：语义，Chris Barrett，Willem Heijltjes，Guy McCusker，2023 [arxiv]
- 微分2-Rigs，Fosco Loregian，Todd Trimble，2022 [arxiv]
- 关于时空的前和前单射结构，James Hefford，Aleks Kissinger，2022 [arxiv]
- 量子机器学习的图示微分，Alexis Toumi，Richie Yeung，Giovanni de Felice，2021 [arxiv]
- 端点范畴学，Fosco Loregian，2020 [arxiv]
- 在MLL中的证明等价性是PSPACE-完全的，Willem Heijltjes，Robin Houston，2016 [arxiv]
- 无单位的线性逻辑，Robin Houston，2013 [arxiv]
- 通过游戏语义将命令式程序视为证明，Martin Churchill，Jim Laird，Guy McCusker，2013 [arxiv]
- 正则表达式包含作为证明搜索问题，Vladimir Komendantsky，2011 [inria]
依赖关系
~2–2.6MB
~71K SLoC