我写了两篇新博客, 关于命题宇宙和类上的投影

ice1000 · 2023 年3 月 28 日 18:01

Inductive Prop are so wrong! | Aya Prover 讨论了命题宇宙和停机性检查之间的交互问题
Class extension with definitional projection | Aya Prover 讨论了 Aya 中的类功能 (或者说「结构体」功能) 的一些设计思想

wuxuan · 2023 年3 月 31 日 23:11

【抱歉歪楼】
记得之前你起草了相关中英术语对照表。
不知有打算给 Aya 的反馈信息逐渐添加中文版本吗？像是:

Clause is redundant
<->
此子句多余，可删除

ice1000 · 2023 年3 月 31 日 23:20

没空做. 不过现在的架构支持「仅通过少量的修改就得到中文版错误信息」. 你只需要找到源码中的 org.aya.util.reporter.Problem 类型 (也就是对应错误信息的类型), 并且将它的如下三个方法

的实现全部翻译成英语即可. 第一个方法实现最多, 一共 88 个子类, 改起来需要较大工作量, 所以我们暂时不会做.

另外我们还有一些新功能正在弄, 马上还要引入稍微多一点的错误信息, 先弄完这些再说.

ice1000 · 2023 年3 月 31 日 23:21

这样可以看到全部的实现, 一个一个跳过去即可.

另外我们也可能不会在官方仓库维护这个功能. 未来可能会想办法扩展编译器接口, 使得这个中文化的过程可以非侵入性地实现.

ice1000 · 2023 年3 月 31 日 23:24

@wuxuan 我现在认为, 数学术语都应该采用香蕉空间的标准. 参见香蕉空间: 写作指引 - 香蕉空间

有关类型论的内容, 我已经整理出写作计划: 模板: 类型论 - 香蕉空间