rename strongestBelief to beliefMergeManyStillBelieved

Author: xieyuheng

TODO.md

@@ -1,3 +1,6 @@
+rename `isBeliefBelieved` to `isStillBelieved`
+extract `beliefMergeMany`
+
 # 4.4 Dependencies Improve Search
 
 > https://github.com/cicada-lang/propagator/issues/4

docs/diary/2024-09-16-propagator-model-and-lattice.md

@@ -0,0 +1,52 @@
+---
+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 的结构是 `Record<Set, Belief>`
+
+用类似 structural subtyping 的方式来统一理解所有 lattice

docs/diary/2024-09-17-solidjs-and-propagator-model.md

@@ -0,0 +1,30 @@
+---
+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 思维。

src/belief-system/assimilateBelief.ts

@@ -15,16 +15,19 @@ export function assimilateBelief<A>(
   // whether the information contained in the new belief is deducible
   // from that in some beliefs already in the belief system. If so, we
   // can just throw the new one away.
+
   if (base.beliefs.some((oldBelief) => isStrongerBelief(oldBelief, belief))) {
     return base
   }
 
   // Conversely, if the information in any existing belief is
   // deducible from the information in the new one, we can throw those
   // existing ones away.
+
   // 注意，对于偏序关系来说，
   // not(lteq(x, y)) 不等于 lteq(y, x)，
   // 前者还包含了偏序关系中不可比较的情况。
+
   const strongerOldBeliefs = base.beliefs.filter(
     (oldBelief) => !isStrongerBelief(belief, oldBelief),
   )

src/belief-system/strongestBelief.ts renamed to src/belief-system/beliefMergeManyStillBelieved.ts

@@ -9,7 +9,7 @@ import { isBeliefBelieved } from "./isBeliefBelieved.js"
 // 注意，这里的 "most informative" 又是就 merge 而言的了，
 // 别忘了 merge 所定义的 implies 与 isStronger 不同。
 
-export function strongestBelief<A>(
+export function beliefMergeManyStillBelieved<A>(
   beliefs: Array<Belief<A>>,
 ): Belief<A> | Nothing {
   const stillBelievedBeliefs = beliefs.filter(isBeliefBelieved)

src/belief-system/beliefSystemMerge.ts

@@ -1,8 +1,8 @@
 import { type MergeConflict } from "../merge-conflict/index.js"
 import { assimilateBelief } from "./assimilateBelief.js"
 import { assimilateBeliefSystem } from "./assimilateBeliefSystem.js"
+import { beliefMergeManyStillBelieved } from "./beliefMergeManyStillBelieved.js"
 import { BeliefSystem } from "./BeliefSystem.js"
-import { strongestBelief } from "./strongestBelief.js"
 
 // Asking the belief system to deduce all the consequences of all its
 // beliefs all the time is perhaps a bad idea, so when we merge belief
@@ -15,6 +15,6 @@ export function beliefSystemMerge<A, B>(
   increment: BeliefSystem<B>,
 ): BeliefSystem<A | B> | MergeConflict {
   const candidate = assimilateBeliefSystem(content, increment)
-  const consequence = strongestBelief(candidate.beliefs)
+  const consequence = beliefMergeManyStillBelieved(candidate.beliefs)
   return assimilateBelief(candidate, consequence)
 }

src/belief-system/beliefSystemQuery.ts

@@ -2,12 +2,12 @@ import { type Belief } from "../belief/index.js"
 import type { Nothing } from "../nothing/Nothing.js"
 import type { BeliefSystem } from "./BeliefSystem.js"
 import { assimilateBelief } from "./assimilateBelief.js"
-import { strongestBelief } from "./strongestBelief.js"
+import { beliefMergeManyStillBelieved } from "./beliefMergeManyStillBelieved.js"
 
 export function beliefSystemQuery<A>(
   beliefSystem: BeliefSystem<A>,
 ): Belief<A> | Nothing {
-  const answer = strongestBelief(beliefSystem.beliefs)
+  const answer = beliefMergeManyStillBelieved(beliefSystem.beliefs)
   const betterBeliefSystem = assimilateBelief(beliefSystem, answer)
   if (beliefSystem !== betterBeliefSystem) {
     beliefSystem.beliefs = betterBeliefSystem.beliefs

src/belief/beliefMerge.ts

@@ -33,21 +33,27 @@ export function beliefMerge<A>(
   // (4) | -- a 与 b 不可比较
 
   if (mergedValue === content.value && mergedValue === increment.value) {
-    // 当 content.value 与 increment.value 等价时，
-    // 取 reasons 更小的，又当 reasons 一样大时，取 content。
+    // - 当 content.value 与 increment.value 相等时，取 reasons 更小的；
+    // - 当 reasons 也相等时，取 content。
+
     // 也就是说，当 content.value 与 increment.value 等价时，
     // 只有当 increment.reasons 真的比 content.reasons 小，才取 increment。
+
+    // 注意，这种取 subset 的行为等价于取 intersection，
+    // 与下面取 union 的行为，在 lattice 的意义上是相互对偶的：
+    // - 在 value 相等时用 intersection，就是用 set lattice。
+    // - 在 value 可比较时，直接取较小 value 的 reasons。
+    // - 在不可比较时用 union，就是用 dual set lattice。
+    // 和 dependent type 类似，这里是 dependent record，
+    // 即后项所取的 lattice 种类，取决于前项的值是否相等。
+
     if (setIsSubsetOf(content.reasons, increment.reasons)) {
       return content
     } else {
       return increment
     }
   }
 
-  // if (isMergeConflict(mergedValue)) {
-  //   console.log({ who: "beliefMerge", increment, content })
-  // }
-
   if (mergedValue === increment.value) {
     return increment
   }