V2EX = way to explore
V2EX 是一个关于分享和探索的地方
现在注册
已注册用户请  登录
xieyuheng
V2EX  ›  数学

「蝉语 / Cicada Language」一个可以用来辅助数学定理之证明的程序语言

  •  1
     
  •   xieyuheng · 171 天前 · 1341 次点击
    这是一个创建于 171 天前的主题,其中的信息可能已经有所发展或是发生改变。

    《蝉语手册》(语言的主要文档): https://readonly.link/manuals/gitlab.com/cicada-lang/cicada

    《蝉语独白》(一个模仿 Little Book 的小册子): https://readonly.link/books/github.com/xieyuheng/cicada-monologues

    项目主页: https://cicada-lang.org

    18 条回复    2022-01-23 16:04:16 +08:00
    xieyuheng
        1
    xieyuheng  
    OP
       171 天前
    欢迎大家转发给可能会感兴趣的朋友捏~
    iamzuoxinyu
        2
    iamzuoxinyu  
       170 天前 via Android
    厉害,虽然我觉得这里的没几个知道什么是 DT 的…
    cmdOptionKana
        3
    cmdOptionKana  
       170 天前
    非常优秀!《蝉语独白》简直可以作为编程的启蒙教材,逻辑清晰得不得了,深入浅出,行文流畅且有文采,页面设计也完全符合平面设计的基本原则,牛人啊。
    lance6716
        4
    lance6716  
       170 天前 via Android
    催更
    xarthur
        5
    xarthur  
       170 天前 via iPhone
    厉害,之前在推特上看到了。
    希望辅助证明的工具越多越好,不过现在看来最大的问题还是学者不大接受这类工具😂
    GeruzoniAnsasu
        6
    GeruzoniAnsasu  
       170 天前
    我看了半天

    「断言」的定义

    但全文没有讲到「断言有什么用」,语言中也没有与断言相关的语法
    afutureus
        7
    afutureus  
       170 天前 via iPhone
    好强
    GeruzoniAnsasu
        8
    GeruzoniAnsasu  
       170 天前
    我又反复看了几遍那篇《蝉语独白》
    然后又看了半天英文那版文档……
    本来还想直接从单测里找 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 ,甚至如何定义公理都没讲明白,更别说推导机制……
    Ultraman
        9
    Ultraman  
       170 天前 via Android
    Emmm 哪位老哥用它来证明一下勾股定理让菜鸡如我理解一下?
    wzzzx
        10
    wzzzx  
       170 天前
    有意思
    imKiva
        11
    imKiva  
       169 天前
    @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
    xieyuheng
        12
    xieyuheng  
    OP
       169 天前
    @Ultraman 这里有对「加法交换律」的证明哦:

    https://readonly.link/manuals/gitlab.com/cicada-lang/cicada/-/datatype/01.1-proving-theorems-about-nat.md
    xieyuheng
        13
    xieyuheng  
    OP
       169 天前
    @cmdOptionKana

    为这个项目努力了很久很久了,还是第一次见到这样的这样的评价。

    有点感动,谢谢你。
    xieyuheng
        14
    xieyuheng  
    OP
       169 天前
    @GeruzoniAnsasu 源码里有非常完备的测试哦。

    详情请见这里的 `tests/`: https://github.com/cicada-lang/cicada/tree/master/docs

    另外,其中的 `manual/` 和 `articles/` 也算是带有文档的测试,运行测试的时候会跑到的。
    xieyuheng
        15
    xieyuheng  
    OP
       169 天前
    @GeruzoniAnsasu 感谢你的反馈!我会仔细思考你提到的点,逐步改进我的文档的。
    lance6716
        16
    lance6716  
       168 天前
    博客有 rss 吗
    xieyuheng
        17
    xieyuheng  
    OP
       167 天前
    @lance6716 目前还没有 rss 。
    不过有 Twitter: https://twitter.com/CicadaLanguage
    和 Telegram:@CicadaLanguageCN
    xieyuheng
        18
    xieyuheng  
    OP
       163 天前
    加了一个 sponsors 页面 https://cicada-lang.org/sponsors
    关于   ·   帮助文档   ·   API   ·   FAQ   ·   我们的愿景   ·   广告投放   ·   感谢   ·   实用小工具   ·   4083 人在线   最高记录 5497   ·     Select Language
    创意工作者们的社区
    World is powered by solitude
    VERSION: 3.9.8.5 · 26ms · UTC 09:23 · PVG 17:23 · LAX 02:23 · JFK 05:23
    Developed with CodeLauncher
    ♥ Do have faith in what you're doing.