connection through half edges

TODO.md

@@ -1,3 +1,15 @@
+# half-edge
+
+[half-edge] `Edge` has two `HalfEdge`s
+
+[half-edge] `HalfEdge` should be a kind of `Value` -- `Port` should quit being a `Value`
+
+[half-edge] avoid using `closeAllFreePorts`
+
+[half-edge] `@edge` as a builtin to create two `HalfEdge`s
+
+[half-edge] refactor
+
 # docs
 
 [docs] add mimor to inet docs

docs/diary/2023-09-17-half-edge.md

@@ -0,0 +1,67 @@
+---
+title: Half edge
+author: Xie Yuheng
+date: 2023-09-17
+---
+
+```
+     \   |   /
+  .-------------.
+  |    \ | /    |
+  |   (.....)   |
+  |      |      |
+  |   (.....)   |
+  |    / | \    |
+  `-------------`
+     /   |   \
+```
+
+> Although during an interaction between two nodes, new nodes and new
+> interactable edges might be introduced, all of the new interactable
+> edges can still be viewed as contained within the circle, during all
+> the new future interactions caused by them, removing and
+> reconnecting will not affect other parts of the graph outside the
+> circle.
+>
+> -- [Programming with interaction nets / section 8](../articles/programming-with-interaction-nets.md#8)
+
+To make implement this, we can not just give each edge an id,
+and make them an entity in the entity store.
+
+Because take the rule between `(zero)` and `(add)` as an example.
+
+```
+     value           value
+       |               |
+     (add)     =>      |
+     /   \              \
+(zero)   addend        addend
+```
+
+After the interaction, the path between `value` and `addend` has two edges.
+
+To reduce this path to one edge again,
+first we might think of deleting edges
+and introduce new edge,
+but we can not to this,
+for nodes outside of the "circle"
+might hold reference to the edges that we want to delete.
+
+One way to handle this (that I can think of),
+is to use `HalfEdge` instead of `Edge`,
+one edge consists of two `HalfEdge`s,
+each `HalfEdge` has an id.
+
+When two edges are connected,
+
+```
+A1|A2 -- B1|B2
+```
+
+we can reduce them to one edge,
+
+```
+A1|B2
+```
+
+without effecting the references to `HalfEdge`s `A1` and `B2`.

docs/diary/2023-09-17-try-prefix-expression.md

@@ -0,0 +1,35 @@
+---
+title: Try prefix expression
+author: Xie Yuheng
+date: 2023-09-17
+---
+
+Postfix expression:
+
+```
+rule zero add
+  (add)-addend
+  return-(add)
+end
+
+rule add1 add
+  (add)-addend
+  (add1)-prev add
+  add1 return-(add)
+end
+```
+
+Prefix expression:
+
+```
+rule zero add {
+  @connect(^add->addend, ^add->return)
+}
+
+rule add1 add {
+  @connect(
+    add1(add(^add1->prev, ^add->addend)),
+    ^add->return,
+  )
+}
+```

experiments/DiffList.i

@@ -0,0 +1,42 @@
+require "List.i"
+
+// Concatenation of lists is performed in linear time
+// with respect to its first argument.
+// Constant time concatenation is possible
+// with difference-lists: the idea consists in
+// plugging the front of the second argument
+// at the back of the first one.
+
+type DiffList @Type -- @Type end
+
+node diff {
+  front: List('A),
+  -------
+  back: List('A),
+  value!: DiffList('A),
+}
+
+
+node diffAppend
+  'A DiffList :target!
+  'A DiffList :rest
+  --------
+  'A DiffList :return
+end
+
+node diffOpen
+  'A DiffList :target!
+  'A List :list
+  ----------
+  'A List :return
+end
+
+rule diff diffAppend
+  (diff)-front diff return-(diffAppend)
+  (diffAppend)-rest diffOpen back-(diff)
+end
+
+rule diff diffOpen
+  (diff)-back list-(diffOpen)
+  (diff)-front return-(diffOpen)
+end

experiments/DiffList.test.i

@@ -0,0 +1,25 @@
+require "DiffList.i"
+require "Trivial.i"
+
+claim oneTwoSoles -- Trivial DiffList end
+
+define oneTwoSoles {
+  let [front, back, value1] = @spread(diff)
+  @connect(front, cons(sole, back))
+  let [front, back, value2] = @spread(diff)
+  @connect(front, cons(sole, cons(sole, back)))
+  diffAppend(value1, value2)
+}
+
+@inspect(oneTwoSoles)
+@inspect(@run(oneTwoSoles))
+
+claim twoTwoSoles -- Trivial DiffList end
+
+define twoTwoSoles
+  (diff) @spread $front sole cons sole cons front @connect
+  (diff) @spread $front sole cons sole cons front @connect
+  diffAppend
+end
+
+twoTwoSoles @inspect @run @inspect

experiments/List.i

@@ -0,0 +1,31 @@
+type List @Type -- @Type end
+
+node null
+  --------
+  'A List :value!
+end
+
+node cons
+  'A :head
+  'A List :tail
+  --------
+  'A List :value!
+end
+
+node append
+  'A List :target!
+  'A List :rest
+  --------
+  'A List :return
+end
+
+rule null append
+  (append)-rest
+  return-(append)
+end
+
+rule cons append
+  (append)-rest (cons)-tail append
+  (cons)-head cons
+  return-(append)
+end

experiments/List.test.i

@@ -0,0 +1,12 @@
+require "List.i"
+require "Trivial.i"
+
+claim sixSoles -- Trivial List end
+
+define sixSoles
+  null sole cons sole cons sole cons
+  null sole cons sole cons sole cons
+  append
+end
+
+sixSoles @inspect @run @inspect

experiments/Nat.i

@@ -0,0 +1,127 @@
+type Nat { -- @Type }
+
+node zero {
+  ------
+  value!: Nat
+}
+
+node add1 {
+  prev: Nat
+  ----------
+  value!: Nat
+}
+
+node add {
+  target!: Nat,
+  addend: Nat
+  --------
+  return: Nat
+}
+
+rule zero add {
+  @connect(^add->addend, ^add->return)
+}
+
+rule add1 add {
+  @connect(
+    add1(add(^add1->prev, ^add->addend)),
+    ^add->return,
+  )
+}
+
+claim one { -- Nat }
+
+define one { add1(zero) }
+
+claim two -- Nat end
+define two one one add end
+
+claim three -- Nat end
+define three two one add end
+
+claim four -- Nat end
+define four two two add end
+
+// To define `mul`, we first need `natErase` and `natDup`.
+
+node natErase
+  Nat :target!
+  --------
+end
+
+rule zero natErase end
+
+rule add1 natErase
+  (add1)-prev natErase
+end
+
+node natDup
+  Nat :target!
+  --------
+  Nat :second
+  Nat :first
+end
+
+rule zero natDup
+  zero first-(natDup)
+  zero second-(natDup)
+end
+
+rule add1 natDup {
+  let first, second = natDup(^add1->prev)
+  @connect(add1(first), ^natDup->first)
+  @connect(add1(second), ^natDup->second)
+}
+
+node mul
+  Nat :target!
+  Nat :mulend
+  --------
+  Nat :return
+end
+
+rule zero mul
+  (mul)-mulend natErase
+  zero return-(mul)
+end
+
+rule add1 mul
+  (mul)-mulend natDup $first $second
+  (add1)-prev first mul second add
+  return-(mul)
+end
+
+// To define `max`, we need `maxAux`.
+
+node maxAux
+  Nat :first
+  Nat :second!
+  --------
+  Nat :return
+end
+
+node max
+  Nat :first!
+  Nat :second
+  ----------
+  Nat :return
+end
+
+rule zero max
+  (max)-second return-(max)
+end
+
+rule add1 max
+  (max)-second (add1)-prev maxAux
+  return-(max)
+end
+
+rule zero maxAux
+  (maxAux)-first add1
+  return-(maxAux)
+end
+
+rule add1 maxAux
+  (add1)-prev (maxAux)-first max
+  add1 return-(maxAux)
+end

experiments/Nat.test.i

@@ -0,0 +1,26 @@
+require "Nat.i"
+require "Nat.i"
+require "Nat.i" // Multiple `require` is fine.
+
+zero zero add @inspect @run @inspect
+two @inspect @run @inspect
+four @inspect @run @inspect
+zero one add @inspect @run @inspect
+
+
+claim addadd Nat Nat Nat -- Nat end
+define addadd add add end
+
+one one one addadd @run @inspect
+
+
+two natErase zero @inspect @run @inspect
+two natDup @inspect @run @inspect
+
+two two mul @inspect @run @inspect
+three three mul @inspect @run @inspect
+
+
+zero two max @run @inspect
+one two max @run @inspect
+three two max @run @inspect

experiments/Trivial.i

@@ -0,0 +1,6 @@
+type Trivial -- @Type end
+
+node sole
+  --------
+  Trivial :value!
+end