逐渐意识到它们不是“遗留”问题，其实是很根本的问题。
问题一： 依赖类型（dependent type）、联合类型（union type）是什么关系？他们是否涉及重新阐释的问题。
我要冒昧地表明用组合关系取消类型本身的独立性如Classless Java是不合理的。比如平面直角坐标系中点（Point）除了两个实数（横坐标和纵坐标）的结合还有其他信息，这在之前群友对我代码的修改中也得到了体现。
这个问题问了实体-关系模型中“实体”从哪里来。
问题二：定理证明是否可以等价于重写（rewriting）。这涉及限制条件（比如EXPRESS中WHERE, REVERSE）的使用和发展。
这个问题应该在数学软件如Matlab的开发过程中就回答过了。
这个问题问了实体-关系模型中“关系”从哪里来。
问题二进展：重写的核心在于其前提——预先定义的规则。这些规则处理的是纯粹形式变化的问题，即所指/语义完全由形式本身确定。
由此可见，数学、物理上的定理证明很多程度是对规则重新定义和梳理的过程，因为那些纷乱的符号和互相孤立的体系（回想中学时突然接触解析几何后应用平面几何知识的转换困难，老师总是批评到：“这不是之前学过的吗，怎么放到平面直角坐标系就不会用了了？！”）。在此不得不回想起王垠对“数学”语言的批判。
Frege-Church本体论和邱奇的后续研究（并不受重视）还没有学习，但能感觉到刚才所提到的“纯粹”模型显然不足以处理现实复杂性，正如乔姆斯基纯句法的思路导致的问题。ps乔姆斯基形式模型的思路与形式规则-重写的思路是一样的。同时要承认纯形式模型本身能解决90%以上问题。
这里的“关系”或许就可以理解成一个函数，有时是函数运行的结果（可视作函数的特例）。比如我部门领导比普通职员每月多赚1500元，这个关系就可以写成（lambda(x) (+ x 1500)），A在X部门工作——(member A (get-staff X)) -> #t
The Little Typer （Daniel Friedman）序言中提到写程序和写定理如走路和骑自行车一样，是一个能力的两个方面。
昨天听一个开题报告，主题是机器学习-语义模型。在他的演示中，语义其实是特殊的形式/句发，通过共现等方式得以体现。我看到他的思路还是句法-形式的方法，于是提问他是不是二者本质一样，这个问题很有意思希望再未来得到回答。
问题二的进展：语义是什么？语义与形式的关系类似连续统假设，不能证明也不能证伪。
目前新了解到的重要理论基础：
1 对布尔代数/离散的逻辑演算的一般化，把它变成可分析函数甚至代数函数，这样把离散系统变成连续系统的特例，打通了离散的、有限的计算机和连续的、无限的现实之间的关系，让信息建模变成可以机器学习的东西。
相关/人物概念：Richard Threlkeld Cox
2 突变理论（Catastrophe Theory）对实现邱奇-弗雷格本体论（concept/symbol-sense-denotation）的意义，它反其道行之，从连续函数开始实现实现了离散关系的模拟，是不是有些机器学习第一节课Sigmoid函数的感觉？
由此看来，信息模型不是什么神秘、无用的东西或废话，而是与计算机程序密不可分的，它的基础根植在概率论和动力系统中。
对相关数学学习的启发：
传统教材中围绕柯尔莫哥洛夫的概率空间，在理解特定问题时比较方便，但不是适合所有人和所有问题。
© 2018-2025 0xFFFF
