diff --git "a/docs/diary/2024-08-29-\345\205\263\344\272\216-TMS-\347\232\204\345\221\275\345\220\215.md" "b/docs/diary/2024-08-29-\345\205\263\344\272\216-TMS-\347\232\204\345\221\275\345\220\215.md" deleted file mode 100644 index bc32452..0000000 --- "a/docs/diary/2024-08-29-\345\205\263\344\272\216-TMS-\347\232\204\345\221\275\345\220\215.md" +++ /dev/null @@ -1,51 +0,0 @@ ---- -title: 关于 TMS 的命名 -date: 2024-08-29 ---- - -之前停下来阅读 "Proposition Networks" 这篇论文， -主要是因为命名上的一些问题。 - -- 首先是对将要实现的 TMS 的命名不满，因为它是个缩写。 -- 其次对 supported-value 也不满，原因是直觉上不满。 - -```typescript -type Support = Set - -type Supported = { - value: A - support: Support -} - -type TMS = { - supportedValues: Array> -} -``` - -再读一遍笔记看看能不能想到好一些的名字。 - -也许应该做如下改变： - -- supported-value -> belief -- TMS -> belief-system - -```typescript -type Reason = Set - -type Belief = { - value: A - reason: Reason -} - -type BeliefSystem = { - beliefs: Array> -} -``` - -用 belief 与 belief-system 也许是不错的选择， -因为在实现类型系统的时候， -cell 代表某个 expression， -而 cell 中的保存的关于 type 的信息， -就是关于命题的信息。 -比如简单的保存一个 type， -就是相信某个 proposition 为真。 diff --git a/docs/diary/2024-09-04-lattice-about-more-informative.md b/docs/diary/2024-09-04-lattice-about-more-informative.md deleted file mode 100644 index a9234b7..0000000 --- a/docs/diary/2024-09-04-lattice-about-more-informative.md +++ /dev/null @@ -1,41 +0,0 @@ ---- -title: Lattice about "more informative" -date: 2024-09-04 ---- - -```typescript -export const merge = defineGeneric() - -export function implies(x: A, y: B): boolean { - return merge(x, y) === x -} -``` - -merge 的效果是让 partial information 变得 more informative。 - -- merge 是 lattice 的 meet。 -- implies 是 ordered set 中的 "less or equal to"。 - 虽然 "more informative" 一词中有一个 "more"， - 但是其实就序集而言它是更小。 - -注意术语所在的领域： - -- merge 是就 partial information 而言的术语。 -- implies 是就命题之间的蕴含而言的术语。 - -最好用例子来理解 "more informative"： - -- 对集合来说，越小的集合越具体，包含的信息更多。 - 比如考虑 CLP(FD) -- Constraint Logic Programming over Finite Domains， - 在求解 constraint 问题的过程中，domain 作为一个集合会变小。 - -- 对于命题来说，蕴含式前项的命题比后项的命题包含更多信息。 - 因此 more informative 就是 implies。 - 集合之间的「包含于」关系，就对应于命题之间「蕴含关系」。 - -- 对区间来说，越小的区间就更精确，就包含更多信息。 - 毕竟，区间是特殊的集合。 - -注意，对于 Belief 来说，merge 所定义的 implies， -与之后定义 beliefSystemMerge 时所用到的 stronger， -对 reasons 集合的理解方式是相反的。 diff --git a/docs/diary/2024-09-16-propagator-model-and-lattice.md b/docs/diary/2024-09-16-propagator-model-and-lattice.md deleted file mode 100644 index c6d17d8..0000000 --- a/docs/diary/2024-09-16-propagator-model-and-lattice.md +++ /dev/null @@ -1,47 +0,0 @@ ---- -title: Propagator Model and Lattice -date: 2024-09-16 ---- - -# Structural Subtyping 作为 Lattice - -Structural Subtyping 作为 Lattice， -可以理解为是一种结构化的构造新的 Lattice 的方式， -已知一些 lattice，然后生成 record lattice。 - -可以理解为带有名字（record 的 key）的 product lattice， -但是与 product 不同的是，key 出现与否可以给出额外的序关系。 - -例如： - -``` -{ a: A, b: B, c: C } <= { a: A, b: B } -{ a: A, b: { x: X, y: Y } } <= { a: A, b: { x: X } } -``` - -一般的集合有： - -``` -{a, b} <= {a, b, c} -``` - -但是当把集合的元素理解为 record 的 key 时，就有： - -``` -{a: Unit, b: Unit, c: Unit} <= {a: Unit, b: Unit} -``` - -# Propagator Model 中的 Lattice - -论文中有 Number、Interval、Belief、BeliefSystem 四种 Lattice。 - -其中： - -- Number 是平凡的。 -- Interval 可以看作是一个 primitive lattice。 -- Belief 和 BeliefSystem 不是简单的 record lattice， - 但是可以看成是以 record lattice 为基础来定义的， - 就像是以 free group 为基础来定义 presentation of a group。 - -Belief 与 BeliefSystem 作为 lattice 之间的关系非常复杂， -要看具体的 merge 函数的定义。 diff --git a/docs/diary/2024-09-17-solidjs-and-propagator-model.md b/docs/diary/2024-09-17-solidjs-and-propagator-model.md deleted file mode 100644 index c745272..0000000 --- a/docs/diary/2024-09-17-solidjs-and-propagator-model.md +++ /dev/null @@ -1,30 +0,0 @@ ---- -title: SolidJS and Propagator Model -date: 2024-09-16 ---- - -solidjs 很明显就是一个 propagator model， -可以理解为 cell 保存的东西是 history -- time 到 value 的 k-v-map， -在前端 view 组件中显示的，只是 history 中最新的 entry。 - -下面的描述和 inet 中用表层语言来构造计算模型的对象类似： - -> Components have a lifecycle that defines how they are created, -> updated, and destroyed. A Solid component's lifecycle is different -> from other frameworks, as it is tied to the concept of reactivity. - -> Where frameworks may re-run components on every state change, a -> Solid component's lifecycle is tied to its initial run. What this -> means is that a Solid component is only run once, when it is first -> rendered into the DOM. After that, the component is not re-run, even -> if the application's state changes. - -> When the Solid component renders, it sets up a reactive system that -> monitors for state changes. When a state change occurs, the -> component will update the relevant areas without re-running the -> entire component. By bypassing the full component lifecycle on -> every state change, Solid has a more predictable behavior compared -> to frameworks that re-run functions on every update. - -但是这里的 "re-run functions on every update" -还是 expression 思维，或者说是 functional 思维。 diff --git a/docs/diary/2024-10-05-searching-by-propagation.md b/docs/diary/2024-10-05-searching-by-propagation.md deleted file mode 100644 index 97fc096..0000000 --- a/docs/diary/2024-10-05-searching-by-propagation.md +++ /dev/null @@ -1,31 +0,0 @@ ---- -title: Searching by Propagation -date: 2024-10-05 ---- - -论文是如何用 propagation networks 来实现搜索的？ -并且还支持了 dependency-directed backtracking。 - -首先，每个解决 constraint processing 问题的系统， -都需要两个功能：searching 和 propagation。 - -将 constraint processing 嵌入在 prolog 一类的逻辑式语言中， -就是在已有 searching 功能的系统中加入 propagation。 - -将 constraint processing 嵌入在 propagation networks 中， -也需要在已有的 propagation 功能之外支持 searching。 - -我觉得这在于用 TMS 记录一个 domain 中所有的选择， -然后 filter 所有的 domain 所组成的笛卡尔积的集合。 - -首先 `(amb cell)` 可以实现 binary choice， -其次用 `amb` 实现的 `(one-of input ... output)` -可以实现在多个 input cells 中的选择， -每个选择会生成有独立 identity 的 reason。 - -发现 contradiction 就可以记录一个 nogood set -（可能带有 one-of 所生成的 reason）， -在 propagation 的过程中，遇到每次遇到 TMS， -都有机会用 nogood set 来 filter TMS 中的 contingent objects。 - -这样就实现了带有 dependency-directed backtracking 的 searching。