「蝉语 / Cicada Language」一个可以用来辅助数学定理之证明的程序语言
xieyuheng · 2022-01-15 12:55:14 +08:00 · 2133 次点击这是一个创建于 1037 天前的主题，其中的信息可能已经有所发展或是发生改变。
《蝉语手册》（语言的主要文档）： https://readonly.link/manuals/gitlab.com/cicada-lang/cicada
《蝉语独白》（一个模仿 Little Book 的小册子）： https://readonly.link/books/github.com/xieyuheng/cicada-monologues
项目主页： https://cicada-lang.org
 |
1
xieyuheng OP 欢迎大家转发给可能会感兴趣的朋友捏～
|
 |
2
iamzuoxinyu 2022-01-15 19:48:35 +08:00 via Android
厉害，虽然我觉得这里的没几个知道什么是 DT 的…
|
 |
3
cmdOptionKana 2022-01-15 20:09:55 +08:00
非常优秀！《蝉语独白》简直可以作为编程的启蒙教材，逻辑清晰得不得了，深入浅出，行文流畅且有文采，页面设计也完全符合平面设计的基本原则，牛人啊。
|
 |
4
lance6716 2022-01-15 23:05:16 +08:00 via Android
催更
|
 |
5
xarthur 2022-01-15 23:45:49 +08:00 via iPhone
厉害，之前在推特上看到了。
希望辅助证明的工具越多越好，不过现在看来最大的问题还是学者不大接受这类工具😂 |
 |
6
GeruzoniAnsasu 2022-01-16 00:27:11 +08:00
我看了半天
「断言」的定义 但全文没有讲到「断言有什么用」，语言中也没有与断言相关的语法 |
 |
7
afutureus 2022-01-16 00:36:10 +08:00 via iPhone
好强
|
|
8
GeruzoniAnsasu 2022-01-16 01:24:08 +08:00
我又反复看了几遍那篇《蝉语独白》
然后又看了半天英文那版文档…… 本来还想直接从单测里找 examples 的但源码里居然没有测试 > We can use check! <exp>: <type>, to make assertion about an expression's type. 看起来「 make assertion 」的含义跟既往理解没什么区别，就是判断一个命题是否正确 但下面的正文里写的意思好像说 「我能为<exp>:<type>下定义」（「我能定义一个<exp>:<type>为真」） 一样。 列举的所有 !check <exp>:<type>我都没看到结论，即断言为真还是假，搞得我一头雾水 -------- 然后在「 built-in types 」这章里塞了 Equal ，本来还以为有什么可等性的定义方法，或者可等类型是什么特殊类型 然而似乎也不是 是说 Equal 这个三元组是一个抽象类型？ 但是又有一句 > If the two elements are actually not the same, we can still use Equal to create a Type, but we can not construct elements of this type …………我就搞不懂了如果「 Equal(X,Y,Z)三元组」这个类型是抽象的，那么去哪，谁来判定 Y 和 Z 是不是相等的？能不能 construct 它的实例到底是怎么判定的？ -------- > If Nat is the most basic datatype, List is the next basic datatype. 我猜原意是「如果说自然数算是最基础的类型，那么 List 可以说是第二基础的」 这个 if 就很没逻辑…… 然后 List( 这个括号里的参数是一个类型对吧，换言之 List(T)是一个泛型，T 作为构造类型的一部分？ 那这样理解的话 Equal()也是一个泛型，List 的参数列表是类型，Equal 里却可以有表达式……为什么？规范是啥…… 然后这一节还似乎想讲讲 list 上的归纳法 我 ctrl+f 了一下没看到 return induction ( 这个 induction 函数是哪讲的就放弃了 我的耐心仅够支撑我研究到这，抱歉…… p.s. 话说启发点是 coq ？文档全文也没看出来如何 prove something ，甚至如何定义公理都没讲明白，更别说推导机制…… |
 |
9
Ultraman 2022-01-16 11:01:30 +08:00 via Android
Emmm 哪位老哥用它来证明一下勾股定理让菜鸡如我理解一下？
|
 |
10
wzzzx 2022-01-16 12:13:06 +08:00
有意思
|
 |
11
imKiva 2022-01-16 17:28:26 +08:00
@GeruzoniAnsasu #8
> 列举的所有 !check <exp>:<type>我都没看到结论，即断言为真还是假，搞得我一头雾水 这个 check! 的意思是要求编译器进行类型检查，即 check <exp> against <type>，如果 <exp> 确实是 <type> 的 inhabitant （或者说 <exp> 具有 <type> 类型），则检查通过。否则应该产生一个类型错误。 > 本来还以为有什么可等性的定义方法，或者可等类型是什么特殊类型。然而似乎也不是。是说 Equal 这个三元组是一个抽象类型？我就搞不懂了如果「 Equal(X,Y,Z)三元组」 「相等类型」相关的内容非常复杂，与这门语言选择的类型论有关。我太菜了，可能回答不了这个问题。 > 那这样理解的话 Equal()也是一个泛型，List 的参数列表是类型，Equal 里却可以有表达式……为什么？规范是啥…… 这是 dependent type （依值类型），即类型可以依赖值。在 DT 的语言中，类型和值并没有什么不同。 > ctrl+f 了一下没看到 return induction ( 这个 induction 函数是哪讲的就放弃了 这个 induction 可以视为「模式匹配」，是编译器内建的操作（比如 rust 的 match ），是一种对归纳数据类型（比如 Nat 类型）归纳证明的一种方法。你可以理解为「分类讨论」。 > 文档全文也没看出来如何 prove something ，甚至如何定义公理都没讲明白 文档这一部分： https://readonly.link/manuals/gitlab.com/cicada-lang/cicada/-/datatype/01.1-proving-theorems-about-nat.md 以加法交换律为例展示了证明，即：add_commute(x: Nat, y: Nat,): Equal(Nat, add(x, y), add(y, x)) 这个函数签名的意思是：对于任意两个自然数 x y ，都有 x + y = y + x 而这个函数的 body 就是对这个命题的证明。 关于这个问题，更多可以参考： https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence |
|
12
xieyuheng OP |
|
13
xieyuheng OP |
|
14
xieyuheng OP @GeruzoniAnsasu 源码里有非常完备的测试哦。
详情请见这里的 `tests/`： https://github.com/cicada-lang/cicada/tree/master/docs 另外，其中的 `manual/` 和 `articles/` 也算是带有文档的测试，运行测试的时候会跑到的。 |
|
15
xieyuheng OP @GeruzoniAnsasu 感谢你的反馈！我会仔细思考你提到的点，逐步改进我的文档的。
|
|
16
lance6716 2022-01-17 19:16:28 +08:00
博客有 rss 吗
|
|
17
xieyuheng OP |
|
18
xieyuheng OP 加了一个 sponsors 页面 https://cicada-lang.org/sponsors
|
Select Language