文件名称：relation-algebra:已归档，因为已在上游进行维护
文件大小：213KB
文件格式：ZIP
更新时间：2024-06-03 11:46:49
Coq
Coq的关系代数 该项目的网页： : 描述 Coq的开发是一个关于关系代数的模块化库：这些代数以异质二元关系作为模型，范围从部分有序的id半体到剩余的Kleene寓言和带有测试的Kleene代数（KAT）。 这个库以模块化的方式展示了这个庞大的代数理论家族。 它包括几种高级自反策略： [kat]，它决定了KAT的（不等式）理论； [hkat]，它决定了KAT的Hoare（不等式）等价理论（即具有Hoare假设的KAT）； [ka]，它决定了KA的（不等式）理论； [ra]，是关系代数的基于归一化的部分决策过程； [ra_normalise]，底层的标准化策略。 Kleene代数的测试策略是通过反射，使用简单的基于双仿真的算法处理适合于KAT的广义正则表达式的，该算法适用于适当的偏导数自动机。 结合KA完整性的形式化和KAT完整性的形式化，这为这些理论的所有模型（包括关系
【文件预览】：
relation-algebra-master
----glang.v(5KB)
----paterson.v(19KB)
----positives.v(2KB)
----mrewrite.mllib(9B)
----bmx.v(4KB)
----untyping.v(26KB)
----rel.v(5KB)
----common.v(4KB)
----lset.v(5KB)
----imp.v(9KB)
----ka_completeness.v(16KB)
----boolean.v(4KB)
----monoid.v(21KB)
----sups.v(8KB)
----description(636B)
----relalg.v(19KB)
----rmx.v(11KB)
----comparisons.v(8KB)
----lattice.v(21KB)
----lang.v(7KB)
----sums.v(2KB)
----level.v(6KB)
----denum.v(2KB)
----kat_dec.mli(1KB)
----matrix.v(22KB)
----ugregex.v(8KB)
----ugregex_dec.v(14KB)
----index.html(32KB)
----move.v(4KB)
----CHANGELOG(911B)
----LICENSE(7KB)
----kat_tac.v(9KB)
----prop.v(2KB)
----kleene.v(7KB)
----traces.v(22KB)
----mrewrite.ml4(4KB)
----kat_dec.ml(5KB)
----kat_reification.ml4(17KB)
----gregex.v(8KB)
----pair.v(4KB)
----powerfix.v(3KB)
----factors.v(3KB)
----dfa.v(6KB)
----ra_fold.ml4(7KB)
----rewriting.v(6KB)
----normalisation.v(25KB)
----matrix_ext.v(9KB)
----ordinal.v(13KB)
----compiler_opts.v(6KB)
----_CoqProject(913B)
----kat_untyping.v(3KB)
----nfa.v(7KB)
----kat_completeness.v(34KB)
----Makefile(336B)
----ra_common.ml(13KB)
----atoms.v(7KB)
----ra_reification.ml4(8KB)
----README.md(3KB)
----syntax.v(15KB)
----ra_reification.mllib(15B)
----COPYING.LESSER(7KB)
----kat_reification.v(9KB)
----COPYING(7KB)
----lsyntax.v(6KB)
----ra.png(17KB)
----kat_reification.mllib(24B)
----deps.sh(546B)
----ra_fold.mllib(8B)
----kat.v(4KB)
----regex.v(16KB)
----ra_common.mllib(10B)