智性哲学世界观
Epistemology and Evolution books/The-Fabric-of-Reality-by-DavidDeutsch
- 生态位类比科学发现中的“问题”
- 复制子replicator类比 knowledge、explanation
- 自然选择 类比 讨论批判
- 最适应的gene 类比 最好的理论
Quantum Mechanics and Computing
- 世界运行基础是量子力学+multiverse
- 物理可行的过程 也是 可以计算模拟的过程
- 有效地模拟世界运行需要量子计算
- 量子计算的高效来自于在多重宇宙中同时计算
- 量子计算只是比经典图灵机等价模型计算更高效，但能力没有差异
Mathematics and Computability Theory
- lambda-calculus 是数学、逻辑学抽象，用来建模“可计算问题”，也可以作为“程序运行规则”
- 图灵机是工程抽象，时间和空间复杂度有直观意义
图灵机和lambda calculus的等价性——图灵机可以计算所有lambda calculus可以model的函数，让计算机科学成为可能 ref https://plato.stanford.edu/archIves/win2024/entries/church-turing
- “丘齐–图灵论题”把人类直觉中的 effective procedure 直接定义成“能被图灵机模拟的过程”。在这种语义下，它是公理式的——“每个有效算法都由图灵机可计算“。“有效”定义如下：
- The Church-Turing thesis concerns the concept of an effective or systematic or mechanical method, as used in logic, mathematics and computer science. “Effective” and its synonyms “systematic” and “mechanical” are terms of art in these disciplines: they do not carry their everyday meaning. A method, or procedure, M, for achieving some desired result is called “effective” (or “systematic” or “mechanical”) just in case:
丘奇-图灵论题涉及逻辑学、数学和计算机科学中使用的"有效"或"系统化"或"机械式"方法的概念。在这些学科中，"有效"及其同义词"系统化"和"机械式"是专业术语：它们并不具有日常含义。当且仅当满足以下条件时，实现某个预期结果的方法或程序 M 被称为"有效的"（或"系统化的"或"机械式的"）： - M is set out in terms of a finite number of exact instructions (each instruction being expressed by means of a finite number of symbols);
M 由有限数量的精确指令组成（每条指令都通过有限数量的符号表达）； - M will, if carried out without error, produce the desired result in a finite number of steps;
M 若正确执行，将在有限步骤内产生预期结果； - M can (in practice or in principle) be carried out by a human being unaided by any machinery except paper and pencil;
M （在实践或理论上）可由人类仅凭纸笔辅助而无需其他机械装置完成； - M demands no insight, intuition, or ingenuity, on the part of the human being carrying out the method.
M 不要求执行者具备洞察力、直觉或独创性。
- 图灵机可执行的程序是effective方法，是不言自明的。逆命题才是核心——“只要存在获取数学函数值的有效方法，该函数就能被图灵机计算。”
- 可有效计算程序和图灵机程序的等价性是可计算等价，而不是”复杂度“等价
- Church-Turing Thesis 是一个被广泛接受的公理性假设，而不是可在系统内部证明的定理。
- 现代版本：
- any algorithmic problem for which we can find an algorithm that can be programmed in some programming language, any language, … is also solvable by a Turing machine. This statement is one version of the so-called Church/Turing thesis. (Harel 1992: 233)
任何能用某种编程语言（无论何种语言）编写算法解决的算法问题，同样也能被图灵机解决。这一陈述就是所谓丘奇/图灵论题的一个版本。（哈雷尔 1992: 233）
“判定性”问题：能否effective判定一个命题的真假
- 当给定一个逻辑或数学命题时，所需流程应能提供完整指导，通过有限步骤的确定性计算来判定该命题正确与否。如此表述的问题，我愿称之为 allgemeine Entscheidungsproblem [普遍判定问题]。（贝曼 1921: 6 [英译 2015: 176]）
- What Turing showed is that there will never be, and can never be, a computing machine satisfying the following specification: When the user types in a formula—any formula—of the functional calculus, the machine carries out a finite number of steps and then outputs the correct answer, either “This formula is provable in the functional calculus” or “This formula is not provable in the functional calculus”, as the case may be. Given, therefore, Turing’s thesis that if an effective method exists then it can be carried out by one of his machines, it follows that there is no effective method for deciding the full first-order functional calculus.
图灵证明的是：未来不会存在、也永远不可能存在满足如下规格的计算机器——当用户输入函数演算中的任意公式时，该机器执行有限步骤后总能输出正确答案："该公式在函数演算中可证"或"该公式在函数演算中不可证"。因此根据图灵论题（若存在有效方法，则必能被其机器执行）可推知：一阶函数演算的完全判定问题不存在有效解决方法。
Extended CT - 加入了计算复杂性 —— 属于经验性假说 尚未被推翻
- There are in fact two different complexity-theoretic versions of the Church-Turing thesis in the modern computer science literature. Both are referred to as the “Extended Church-Turing thesis”. The first was presented by Yao in 2003:
现代计算机科学文献中实际上存在两种不同的丘奇-图灵论题复杂性理论版本，均被称为"扩展版丘奇-图灵论题"。第一种由姚期智在 2003 年提出：- The Extended Church-Turing Thesis (ECT) makes the … assertion that the Turing machine model is also as efficient as any computing device can be. That is, if a function is computable by some hardware device in time T(n)T(n) for input of size nn, then it is computable by a Turing machine in time (T(n))k(T(n))k for some fixed kk (dependent on the problem). (Yao 2003: 100–101)
扩展版丘奇-图灵论题（ECT）主张...图灵机模型在计算效率上与其他任何计算设备相当。即，如果某函数可被硬件设备在规模为 nn 的输入上以 T(n)T(n) 时间计算，则该函数也可由图灵机在 (T(n))k(T(n))k 时间内计算，其中 kk 为与问题相关的固定参数。（姚 2003: 100–101）
- Yao points out that ECT has a powerful implication:
姚指出 ECT 具有重要推论：- at least in principle, to make future computers more efficient, one only needs to focus on improving the implementation technology of present-day computer designs. (2003: 101)
至少在理论上，要使未来计算机更高效，只需专注于改进现有计算机设计的实现技术即可。（2003: 101）
Physical CT - 考虑实际物理系统而不只是理论上的“有效可计算” —— 也是经验假说：
- Deutsch-Wolfram Thesis: 多伊奇-沃尔夫拉姆命题：
Every finite physical system can be simulated to any specified degree of accuracy by a universal Turing machine. (Copeland & Shagrir 2019)
任何有限物理系统都能被通用图灵机以任意指定精度模拟。（科普兰与沙格里尔 2019）
- 哥德尔不完备 定理思路的一些应用：
- 存在图灵机无法计算的实数
- 存在Lean无法证明的定理
- 任何可递归枚举且一致的证明助理（Lean、Coq、Agda、Isabelle …）都必然“漏掉”某些对 ℕ 的真命题；而且这些漏掉的命题既包括精心构造的“怪句”，也包括数学家在意的重大命题；它们的形态既可以是存在性断言，也可以是否定或等价类的断言。
- 逻辑与悖论
- 朴素集合论
- 罗素悖论
- 避免罗素悖论的集合论 ZF、ZFC集合论
- 哥德尔不完备第一、第二定理
- 分形
- category theory and type theory
Mathematics is the art of giving the same name to different things
- Group theory ≈ symmetry + action
- Ring theory ≈ arithmetic + algebraic geometry + representations
- Graph theory ≈ relations + structure on networks
- category theory: morphisms and universal patterns
- Topology “study of continuity” — properties preserved under squishing/stretching.
- Measure theory “study of size” — generalised length/area/probability.
- Functional analysis “linear spaces of functions” — infinite-dimensional linear algebra + topology.
- Differential geometry “calculus on curved spaces” — manifolds, curvature, geodesics.
- Combinatorics “art of counting & arranging” — discrete structures.
- type as proposition
- terms (element(s) in a type) as proof; program as proof
- Proof could be written as program -> Lean/Coq/Agoda
- Program could be interpreted as proof