Abstract. 一些多元微积分的内容,严格来说和 Tensor 关系不大,和 Vector 关系比较大。就当是学物理了。

之前看过一次这一章,实际上没怎么看懂,写的东西很不得要领,于是删了重写。

Read more »

Abstract. 是谁没有 Mac 也没装 Linux 就来选 Software Fundations 啊🤣👉

原来是我🤡🤡🤡

讲一下今晚上配置 coq 环境的流程以及踩的所有坑。其实可能有的地方记不太清楚了。

配置时间和环境:2024. 2. 22,本地环境为 Windows 11 22621.3155,vscode 1.86.2,wsl 发行版为 Ubuntu 22.04,但是感觉未必需要对着配置。

Keywords. 环境配置, wsl, WSL_E_CONSOLE, Coq, VsCoq, opam。

Read more »

Abstract. 最不想学 FP 的一集《三句话让我写了一晚上形式化验证》。

本文讲如何在 Agda 中定义《数理逻辑与集合论 (1) 命题逻辑》中提到的演绎系统,并形式化验证了文中的几个定理。

好像现在我们的姿势还不太正确,我们确实找到了一种方法来验证一个证明对不对,但是对自己证明定理没有一点帮助(甚至有负贡献)。

Read more »

Abstract. 从语义的角度来看谓词逻辑,对应书上的第四、第五章。因为听说 thu 没学 6789 章,猜测可能是难度比较大,故在这里断章。

Read more »

Abstract. 命题逻辑相关的内容,跳过了众所周知的内容,写一些以前没见过的。

第一节主要从语义角度讨论命题逻辑的等值和推理,第二节从语法角度讨论命题逻辑的公理系统,以完备性(和可靠性,但是这里没写)作为连接两者的桥梁。在开头简单阐释一下语义和语法的概念:语义意义下任何等值的变换都可以接受,语法意义下只有变换规则给出的变换可以接受。

参考资料是 thu 的数理逻辑与集合论教材。

Read more »

Abstract. 本节考虑下图所示的通信模型,对 source 和 channel 部分进行建模,并给出几个与 source 的特性和 channel 的承载率相关的定理(Kraft Inequality,Gibbs Inequality,Source Coding Theorem,Noise Channel Theorem)。

Read more »
0%