diff --git a/docs/diary/2023-07-27-design-of-new-syntax.md b/docs/diary/2023-07-27-design-of-new-syntax.md deleted file mode 100644 index 7bd92d83..00000000 --- a/docs/diary/2023-07-27-design-of-new-syntax.md +++ /dev/null @@ -1,180 +0,0 @@ ---- -title: Design of New Syntax -author: Xie Yuheng -date: 2023-07-27 ---- - -# Nat - -Use `defnode` to define a node. - -`--` separates input ports from output ports in the definition. - -Use `!` as postfix to mark the principal port. - -```inet -defnode zero -- return: Nat! end - -defnode add1 prev: Nat -- return: Nat! end - -defnode add x: Nat! y: Nat -- return: Nat end -``` - -If there is only one output port, -the `return` is the default name, -thus can be omitted. - -```inet -defnode zero -- Nat! end - -defnode add1 prev: Nat -- Nat! end - -defnode add x: Nat! y: Nat -- Nat end -``` - -Use `defrule` to define a rule, -use `()-` to push port to the stack, -use `-()` to weld a port to the top port on the stack. - -```inet -defrule zero add - (add)-y return-(add) -end - -defrule add1 add - (add1)-prev - (add)-y - add add1 - return-(add) -end -``` - -`defru` is a short hand for simple `defrule`. - -```inet -defru zero add end - -defru add1 add add add1 end -``` - -```inet -defn two - zero add1 - zero add1 - add -end - -defn four - two two add -end -``` - -# List - -We use a simple type system like Haskell (for now). - -```inet -defnode sole -- Trivial! end - -defnode null -- List('A)! end - -defnode cons - head: List('A) - tail: List('A) - -- List('A)! -end - -defnode append - left: List('A)! - right: List('A) - -- List('A) -end - -defrule null append - (append)-right return-(append) -end - -defrule cons append - (cons)-tail (append)-right append - (cons)-head cons - return-(append) -end - -defru null append end - -# the syntax for `let` and `get` is yet to be designed. -# I use `<...>` and description for work-in-progress syntax design. - -defru cons append - append cons -end - -defn sixSoles - null sole cons sole cons sole cons - null sole cons sole cons sole cons - append -end -``` - -# DiffList - -```inet -defnode diff - left: List('A) - right: List('A) - -- DiffList('A)! -end - -defnode diffAppend - left: DiffList('A)! - right: DiffList('A) - -- DiffList('A) -end - -defnode diffOpen - DiffList('A)! - list: List('A) - -- List('A) -end - -defrule diff diffAppend - (diff)-right (diffAppend)-right diffOpen - (diff)-left diff -end - -defrule diff diffOpen - (diff)-right list-(diffOpen) - (diff)-left return-(diffOpen) -end - -defru diff diffAppend - - - diffOpen diff -end - -defru diff diffOpen - - connect - -end -``` - -`wire` places the two ports of a special edge on the stack. - -If a wire's two ports are connected with port `A` and `B`, -after building a net, we remove the wire, and connect `A` with `B`. - -```inet -defn oneTwoSoles - wire sole cons diff - wire sole cons sole cons diff - diffAppend -end - -defn twoTwoSoles - wire sole cons sole cons diff - wire sole cons sole cons diff - diffAppend -end -``` diff --git a/docs/diary/2023-07-28-procedural-programming-as-macro-system.md b/docs/diary/2023-07-28-procedural-programming-as-macro-system.md deleted file mode 100644 index dacb0191..00000000 --- a/docs/diary/2023-07-28-procedural-programming-as-macro-system.md +++ /dev/null @@ -1,29 +0,0 @@ ---- -title: Procedural programming as macro system -author: Xie Yuheng -date: 2023-07-28 ---- - -For graph-based programming model, -we do not have a static syntax, -our syntax is actually a stack-based -procedural programming language -for building graph. - -We can make the procedural part of the language more powerful, -so that itself is a general programming language. - -Thus, what can be putted on the stack, -is not only ports, but also strings, numbers and objects. - -Like in graph database, where a node in graph is a container, -in which there can be an object. -Maybe we can view our graph as container too. - -For syntax of a graph-based language, it is obvious that -we need to use powerful computation to construct the syntax, -is this also true for other syntax? -For examples, more complicated one like cell-complex, -and more simple one like tree. - -- See minimalist program of generative grammar. diff --git a/docs/diary/2023-07-28-using-string-for-local-variable.md b/docs/diary/2023-07-28-using-string-for-local-variable.md deleted file mode 100644 index 2f7f9784..00000000 --- a/docs/diary/2023-07-28-using-string-for-local-variable.md +++ /dev/null @@ -1,19 +0,0 @@ ---- -title: Using string for local variable -author: Xie Yuheng -date: 2023-07-28 ---- - -We can use string to implement local variable, -to get pure postfix syntax. - -```inet -defn cons append - "head" set append - "head" get cons -end -``` - -How about keywords like `set`, but need a code block? - -TODO diff --git a/docs/diary/2023-07-29-interaction-nets-and-logic-programming.md b/docs/diary/2023-07-29-interaction-nets-and-logic-programming.md deleted file mode 100644 index 33277aa1..00000000 --- a/docs/diary/2023-07-29-interaction-nets-and-logic-programming.md +++ /dev/null @@ -1,10 +0,0 @@ ---- -title: Interaction Nets and Logic Programming -author: Xie Yuheng -date: 2023-07-29 ---- - -From the example of `DiffList`, we know that -iNet is like linear logic programming. - -TODO diff --git a/docs/diary/2023-07-30-neutral-sign.md b/docs/diary/2023-07-30-neutral-sign.md deleted file mode 100644 index 9993c022..00000000 --- a/docs/diary/2023-07-30-neutral-sign.md +++ /dev/null @@ -1,22 +0,0 @@ ---- -title: Neutral Sign -author: Xie Yuheng -date: 2023-07-30 ---- - -To implement cut for wire, -beside positive sign (for output) and negative sign (for input), -we also need neutral sign. - -A type with neutral sign can be matched with both -positive sign and negative sign, so that -a wire can be composed with both input port -and output port, then the port of the wire become the given sign -and other port of the wire become the opposite sign. - -This might be an unwanted complicity, -but to avoid using neutral sign, -we need to avoid using wire, -and design new syntax to apply a node -not only in the default way --- matching inputs and push outputs to the stack. diff --git a/docs/diary/2023-07-30-parallelization.md b/docs/diary/2023-07-30-parallelization.md deleted file mode 100644 index 2587864e..00000000 --- a/docs/diary/2023-07-30-parallelization.md +++ /dev/null @@ -1,22 +0,0 @@ ---- -title: Parallelization -author: Xie Yuheng -date: 2023-07-30 ---- - -Building a net and interact a rule -are using the same context (`mod` and `net`), -but actually `interact` also has -current active edge, to support syntax -like `-()` and `()-`. - -We can let `Net` has `currentActiveEdge`, -since we already can not do parallelization -because we are sharing the stack, -and JS is single thread language. - -We can also make `activeEdge` and -optional argument of `Word.apply`. - -To do parallelization `currentActiveEdge` -and the stack need to be context of `interact`. diff --git a/docs/diary/2023-07-31-signed-ports-vs-signed-types.md b/docs/diary/2023-07-31-signed-ports-vs-signed-types.md deleted file mode 100644 index 56195ed7..00000000 --- a/docs/diary/2023-07-31-signed-ports-vs-signed-types.md +++ /dev/null @@ -1,15 +0,0 @@ ---- -title: Signed Ports v.s. Signed Types -author: Xie Yuheng -date: 2023-07-31 ---- - -In the "Interaction Nets" paper, -Yves Lafont used signed types instead of signed ports. - -In our implementation we use signed ports (input or output), -instead of signed types (types are kept simple). - -For type checking the two ways are the same, -because if we use signed types, when defining a node, -the signs of its ports are given by the types staticly. diff --git a/docs/diary/2023-08-02-defdata.md b/docs/diary/2023-08-02-defdata.md deleted file mode 100644 index 4e200821..00000000 --- a/docs/diary/2023-08-02-defdata.md +++ /dev/null @@ -1,57 +0,0 @@ ---- -title: defdata -author: Xie Yuheng -date: 2023-08-02 ---- - -We can use `defdata` to `deftype` and `defnode` (constructor) together. - -# Nat - -Instead of - -```inet -deftype Nat 0 end -defnode zero -- value!: Nat end -defnode add1 prev: Nat -- value!: Nat end -``` - -We can write - -```inet -defdata Nat - zero -- value!: Nat end - add1 prev: Nat -- value!: Nat end -end -``` - -# List - -Instead of - -```inet -deftype List 1 end -defnode null -- value!: List('A) end -defnode cons head: 'A, tail: List('A) -- value!: List('A) end -``` - -We can write - -```inet -defdata List('A) - null -- value!: List('A) end - cons head: 'A, tail: List('A) -- value!: List('A) end -end -``` - -Maybe we can use `a` instead of `'A`, -because `defdata List(a)` introduces `a` into the scope. - -But the eliminator like `append` still need to use `'A`. - -```inet -defdata List(a) - null -- value!: List('A) end - cons head: a, tail: List(a) -- value!: List(a) end -end -``` diff --git a/docs/diary/2023-08-07-use-pure-postfix-syntax.md b/docs/diary/2023-08-07-use-pure-postfix-syntax.md deleted file mode 100644 index 043b14d8..00000000 --- a/docs/diary/2023-08-07-use-pure-postfix-syntax.md +++ /dev/null @@ -1,87 +0,0 @@ ---- -title: Use pure postfix syntax -author: Xie Yuheng -date: 2023-08-07 ---- - -We should use pure postfix syntax. - -# Nat - -**Prefix type term**: - -```inet -type Nat 0 end -node zero -- value!: Nat end -node add1 prev: Nat -- value!: Nat end - -node add target!: Nat addend: Nat -- return: Nat end - -node add - target!: Nat - addend: Nat - ------------ - return: Nat -end -``` - -**Pure postfix**: - -```inet -type Nat Type end -node zero -- Nat :value! end -node add1 Nat :prev -- Nat :value! end - -node add Nat :target! Nat :addend -- Nat :return end - -node add - Nat :target! - Nat :addend - ------------ - Nat :return -end -``` - -# List - -**Prefix type term**: - -```inet -type List 1 end -node null -- value!: List('A) end -node cons head: 'A tail: List('A) -- value!: List('A) end - -node append target!: List('A) rest: List('A) -- return: List('A) end - -node append - target!: List('A) - rest: List('A) - -------- - return: List('A) -end -``` - -**Pure postfix**: - -```inet -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 - -node append - 'A List :target! - 'A List :rest - -------- - 'A List :return -end -``` - -# About JSON - -When designing syntax I have a goal to be able to -write JSON directly in the language. - -We should give up this goal, -because it is too limiting for new syntax design. diff --git a/docs/diary/2023-08-08-dependent-type-system.md b/docs/diary/2023-08-08-dependent-type-system.md deleted file mode 100644 index fde8bd5f..00000000 --- a/docs/diary/2023-08-08-dependent-type-system.md +++ /dev/null @@ -1,82 +0,0 @@ ---- -title: dependent type system -author: Xie Yuheng -date: 2023-08-08 ---- - -Simple type system is easy to implement, -how about dependent type system? - -If we can implement equality between `Net`s, -we can use `Net` as value. - -# An information analysis of dependent type system - -In a dependent type system, we have - -``` -check(ctx: Ctx, exp: Exp, t: Type) -``` - -The total information of `exp` is available to `check`. - -But for our `cut`, it is actually `infer` + `compose`. - -One word has two levels of information. - -After `infer` the first level of information of a word is not available anymore, -only the second level of the information of the word is available. - -This is why we can not have dependent type system -for the current design -- a design using `cut`. - -# Type checking for interaction nets - -Type checking for interaction nets can actually be simpler. - -We do NOT need to implement a function like `check`, -or implement `cut` as `infer` + `compose`. - -We can simply do type checking by building the net, -when connecting two ports during building the net, -check the signs of the two ports -and unify the types of the two ports. - -Remember, in inet, we can build a net without running it! - -In type system of normal language, -type checking happens during building the syntax tree. -In inet, the net is the syntax, -type checking happens during building the net. - -# Type checking of rules - -Type checking of `rule` can obviously be done by building the local net. - -# Type checking of word definitions - -Type checking of `claim` and `define` can also be done by -first preparing some input ports on the stack -then building the local net. - -Because every port is of some node, -thus to prepare ports, we need to introduce nodes. - -We can introduce single-port nodes from types, -where will be no rules defined for such nodes, -they are not interactive, merely placeholders. - -# Partial evaluation - -Dependent type system need to perform partial evaluation -to check equivalent of two functions. - -Partial evaluation is trivial for inet! - -# Conclusion - -We do not need `cut`, we can just check the words by building the net. - -This means we will have a dynamicly typed (or simply typed) -postfix general programming language -as a macro system. diff --git a/docs/diary/2023-08-27-port-should-connect-to-edge-instead-of-port.md b/docs/diary/2023-08-27-port-should-connect-to-edge-instead-of-port.md deleted file mode 100644 index 782629b1..00000000 --- a/docs/diary/2023-08-27-port-should-connect-to-edge-instead-of-port.md +++ /dev/null @@ -1,15 +0,0 @@ ---- -title: Port should connect to edge instead of port -author: Xie Yuheng -date: 2023-08-27 ---- - -In a shared-memory multithread implementation, -port must connect to edge instead of port, -so that parallel updates of the net will not -interfere with each other. - -Since JavaScript is singlethread -this does not matter, -but as a reference implementation -port still should connect to edge instead of port. diff --git a/docs/diary/2023-09-05-to-learn.md b/docs/diary/2023-09-05-to-learn.md deleted file mode 100644 index bb63133f..00000000 --- a/docs/diary/2023-09-05-to-learn.md +++ /dev/null @@ -1,17 +0,0 @@ ---- -title: To learn -author: Xie Yuheng -date: 2023-09-05 ---- - -Phase space and monoid -- understand the model theory of linear logic. - -Coherent space -- understand the denotational semantics of linear logic. - -Understand proof-nets for all connectives. - -- proof-nets--the-parallel-syntax-for-proof-theory--1995.pdf -- "The linear abstract machine", Lafont, 1990. -- "From proof-nets to interaction net", Lafont, 1995 - -Use inet to encode lambda calculus. diff --git a/docs/diary/2023-09-13-refactor-the-syntax-of-rearrange-to-literal-node-and-spread.md b/docs/diary/2023-09-13-refactor-the-syntax-of-rearrange-to-literal-node-and-spread.md deleted file mode 100644 index 9efa8ab3..00000000 --- a/docs/diary/2023-09-13-refactor-the-syntax-of-rearrange-to-literal-node-and-spread.md +++ /dev/null @@ -1,65 +0,0 @@ ---- -title: Refactor the syntax of rearrange to literal node and spread -author: Xie Yuheng -date: 2023-09-13 ---- - -To construct `DiffList`, I previously design a syntax -to rearrange a node's port before applying it. - -Before rearrange: - -``` - return - | - (cons) - / \ -head tail -``` - -after rearrange by `(cons :tail)`, -the port `tail` will be changed -from an input position to an output position -(it is still an input port). - -``` - tail return - \ / - (cons) - | - head -``` - -Example usage to construct `DiffList`: - -``` -zero (cons :tail) zero cons diff $value @connect value -zero (cons :tail) zero cons diff $value @connect value -diffAppend -``` - -Now the syntax of rearrange is removed, -and I use `(node)` to create a node, -and `@spread` to get all it's ports. - -``` -(diff) @spread $front $back $value -back zero cons zero cons front @connect value -(diff) @spread $front $back $value -back zero cons zero cons front @connect value -diffAppend - -// use less variables: - -(diff) @spread $front $back -back zero cons zero cons front @connect -(diff) @spread $front $back -back zero cons zero cons front @connect -diffAppend - -// use less variables: - -(diff) @spread $front zero cons zero cons front @connect -(diff) @spread $front zero cons zero cons front @connect -diffAppend -``` diff --git a/docs/diary/2023-09-13-syntax-for-referencing-target-ports-in-a-rule.md b/docs/diary/2023-09-13-syntax-for-referencing-target-ports-in-a-rule.md deleted file mode 100644 index 7065e30c..00000000 --- a/docs/diary/2023-09-13-syntax-for-referencing-target-ports-in-a-rule.md +++ /dev/null @@ -1,64 +0,0 @@ ---- -title: Syntax for referencing target ports in a rule -author: Xie Yuheng -date: 2023-09-13 ---- - -In the definition of a rule: - -``` -rule add1 add - (add)-addend - (add1)-prev add - add1 return-(add) -end -``` - -We need to reference the target ports of the two target nodes. - -I used `(node)-port` to push a port to the stack, -and `port-(node)` to connect a port to the top port in the stack. - -This is because in the ASCII art of rule: - -``` - return value - | | - (add) => (add1) - / \ | -(add1) addend (add) - | / \ -prev target addend -``` - -Connection is written as: - -``` -(add)--(add1) -``` - -If we also write the port names, we get: - -``` -(add)-target return-(add1) -``` - -This format is also used to print an edge. - -# Ad-hoc-ness of this syntax - -The `(node)-port` and `port-(node)` syntax feels ad-hoc, because - -- They can only be used in the definition of a rule. -- `(node)-port` is viewed as a whole, not `(node)` and `-port`. -- `(node)-port` does not represent a port of `(node)`, - but represents a port that is exposed by removing `(node)`, - this might be confusing. - -# The semantic as a linear store - -The semantic of `(node)-port` and `port-(node)`, -is like fetching value out of a linear store. - -Linear, because once a value is fetched, it is consumed, -and can not be fetched again. diff --git a/docs/diary/2023-09-17-half-edge.md b/docs/diary/2023-09-17-half-edge.md deleted file mode 100644 index dcc4e037..00000000 --- a/docs/diary/2023-09-17-half-edge.md +++ /dev/null @@ -1,67 +0,0 @@ ---- -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`. diff --git a/docs/mimors/interaction-combinators.mimor b/docs/mimors/interaction-combinators.mimor deleted file mode 100644 index 45c890d7..00000000 --- a/docs/mimors/interaction-combinators.mimor +++ /dev/null @@ -1,12 +0,0 @@ - - - - "Interaction Combinators", Yves Lafont, 1997. - - This paper is the continuation of - the author's work on interaction nets, - inspired by Girard's proof nets for linear logic. - diff --git a/docs/mimors/interaction-nets.mimor b/docs/mimors/interaction-nets.mimor deleted file mode 100644 index 4aea52ba..00000000 --- a/docs/mimors/interaction-nets.mimor +++ /dev/null @@ -1,207 +0,0 @@ - - - - "Interaction Nets", Yves Lafont, 1990. - - - - Interaction net (iNet) is a computation model - based on (indirected) graph. - - - - What is computation? - - - Computation is directed changes. - - - - - What is a computation model? - - - A computation model is a group of rules about how to change. - - - - - What is a program? - - - A program is an initial state of a computation model, - ready to change. - - - - - What is a net of interaction nets? - - - A net is an undirected graph, - where each node has finite list of input ports, - and a finite list of output ports. - - A connection between nodes must go through ports. - - - - - What is the "interaction" of interaction nets? - - - Interaction is graph rewriting based on rules - which have the following constraints: - - 1. linearity - - 2. binary interaction - - 3. no ambiguity - - 4. optimisation - - - - - What is the "linearity" constraint of interaction rules? - - - Inside a rule, each variable port occurs exactly twice, - once in the left side of the rule and -. once in the right side of the rule. - - - - - What is the "binary interaction" constraint of interaction rules? - - - Each node has one principal port. - - Nodes interact through their principal port only. - - An edge connecting two principal ports is called alive or active. - - - - - What is the "no ambiguity" constraint of interaction rules? - - - There is at most one rule for each pair of distinct nodes S, Z, - and no rule for the node with itself S, S. - - - - - What is the "strong confluence" of rewriting system? - - - Strong confluence of a rewriting system means: - - If N reduces in one step to P and Q, - with P != Q, then P and Q reduce - in one step to a common R. - - Strong confluence means that - the relative order of concurrent - reductions is completely irrelevant. - - - - - Prove interaction has strong confluence. - - - By "binary interaction" and "no ambiguity", - rules apply to disjoint pairs of nodes, - and cannot interfere with each other. - - By "linearity" interactions are purely local - and can be performed concurrently. - - - - - What is the "optimisation" constraint of interaction rules? - - - The right side of a rule contains no active edge. - - - - - Does the "optimisation" constraint of interaction rules - ensures termination? - - - No. - - The simplest counterexample is the turnstile. - - TODO code of turnstile - - - - - What is a well typed net? - - - A net is well typed if inputs are connected to - outputs of the matching type. - - - - - What is a well typed rule? - - - A rule is well typed if: - - (1) In the left side of the rule, - one principal is input and another is output, - and they have matching types. - - (2) The right side of the rule is well typed, - where the types of variable ports - are given by the left side. - - - - - What is the "completeness" constraint of well typed interaction rules? - - - There is a rule for each pair of matching nodes. - - Thus all active edge can be reduced. - - - - - A node is called constructor if its principal port - is an output port. - - A node is called eliminator if its principal port - is an input port. - - - - Let N be a net with some free ports. - - If N is well typed, finite and nonempty. - - What is the characteristic of N being irreducible? - - - And if N is irreducible, - then starting from any node, - you can follow principal ports - until you reach a free ports - or you loop! - -