diff --git a/TODO.md b/TODO.md index 4f981cca..ecfa6cc2 100644 --- a/TODO.md +++ b/TODO.md @@ -1,7 +1,3 @@ -回顾 linear logic - -- linear logic 的谓词演算是什么样的？ - `NodeId` vs `Node` -- instead of `Node` vs `NodeEntry` -- the same for `HalfEdge` static import should handled by an extra pass -- instead of injecting a `Loader` to `Mod` Type as Value -- 用 HalfEdge 来编码 Type -- 删除 TypeCtor | Type | Symbol | TypeTerm 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 2e6cd5a1..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 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/diary/2023-09-17-try-prefix-expression.md b/docs/diary/2023-09-17-try-prefix-expression.md deleted file mode 100644 index bf11a4ee..00000000 --- a/docs/diary/2023-09-17-try-prefix-expression.md +++ /dev/null @@ -1,35 +0,0 @@ ---- -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, - ) -} -``` diff --git a/docs/diary/2023-09-20-applicative-syntax-contains-more-information-than-concatenative-syntax.md b/docs/diary/2023-09-20-applicative-syntax-contains-more-information-than-concatenative-syntax.md deleted file mode 100644 index e4ee1c8f..00000000 --- a/docs/diary/2023-09-20-applicative-syntax-contains-more-information-than-concatenative-syntax.md +++ /dev/null @@ -1,17 +0,0 @@ ---- -title: Applicative syntax contains more information than concatenative syntax -author: Xie Yuheng -date: 2023-09-20 ---- - -Due to the use of explicit barcket, -applicative syntax contains more information than concatenative syntax. - -With explicit barcket, we can use auto curry. - -Since applicative syntax contains more information, -we need to hold less information in our human memory. - -It also does not make sense to compile to concatenative syntax, -because compilation is a kind of elaboration, -and elaboration should increase information. diff --git a/docs/diary/2023-09-20-no-closure.md b/docs/diary/2023-09-20-no-closure.md deleted file mode 100644 index 59db5b8d..00000000 --- a/docs/diary/2023-09-20-no-closure.md +++ /dev/null @@ -1,30 +0,0 @@ ---- -title: No closure -author: Xie Yuheng -date: 2023-09-20 ---- - -We have top level `function` keyword, -but we do not have closure. - -Because it does not make sense for closure to capture linear local variables. - -And the semantic of `function` is actually like `node`. - -Imagining we have a keyword `net`. - -The semantic of `addadd` - -``` -function addadd(x: Nat, y: Nat, z: Nat): Nat { - return add(add(x, y), z) -} -``` - -is actually - -``` -net addadd(x: Nat, y: Nat, z: Nat -- result: Nat) { - @connect(result, add(add(x, y), z)) -} -``` diff --git a/docs/diary/2023-09-20-optimization-of-function-body-by-partial-evaluation.md b/docs/diary/2023-09-20-optimization-of-function-body-by-partial-evaluation.md deleted file mode 100644 index 52c7263e..00000000 --- a/docs/diary/2023-09-20-optimization-of-function-body-by-partial-evaluation.md +++ /dev/null @@ -1,12 +0,0 @@ ---- -title: Optimization of function body by partial evaluation -author: Xie Yuheng -date: 2023-09-20 ---- - -Optimization of the evaluation of function body and rule body, -can be done by partial evaluate the function during definition, -to get the graph it should build, -so that at run time, we only need to clone the graph. - -To do this, we need a way to clone a graph with new id. diff --git a/docs/diary/2023-09-25-how-to-do-practical-programming.md b/docs/diary/2023-09-25-how-to-do-practical-programming.md deleted file mode 100644 index 8b63b777..00000000 --- a/docs/diary/2023-09-25-how-to-do-practical-programming.md +++ /dev/null @@ -1,22 +0,0 @@ ---- -title: How to do practical programming -author: Xie Yuheng -date: 2023-09-25 ---- - -How to use inet to do practical programming? - -We need to do side effects such as file IO. - -- Maybe every side effects can be viewed as assignment? - -We need to handle number and string. - -- Maybe just view string as list of chars, - and view char and number as special node. - -- Maybe we can use special node to add number. - -We need to handle JSON. - -- Maybe just use association list to represent record. diff --git a/docs/diary/2023-11-30-parallel-inet.md b/docs/diary/2023-11-30-parallel-inet.md deleted file mode 100644 index d500c98e..00000000 --- a/docs/diary/2023-11-30-parallel-inet.md +++ /dev/null @@ -1,51 +0,0 @@ ---- -title: Parallel iNet -date: 2023-11-30 ---- - -# Problem - -To implement parallel interaction nets, -we need to let many threads share the same memory. - -To allocate memory of cells of the same size, -we can use an array, and a stack of unused indexes -(let's call this free-stack). - -But the stack will still be the part where multi-thread is not safe -right? If any part of the implementation is not lock-free, the fine -grain parallel advantage of inet might be lost. - -# Solution A - -Maybe i can just use 8 "free-stacks" for 8 threads. - -When a used index is to be freed, i can see which thread is having the -least free indexes, and give the new freed index to it. - -And a "free-stack" can be viewed as a ring, i give back to the front -instead of the end, thus lock-free. - -The query about "the least free indexes" is just heuristic, thus also -lock-free. - -# Datatypes - -I need to allocate the following kinds of datatypes: - -``` -Node { - definition: NodeDefinition - ports: List -} - -Port { - node: Node - halfEdge?: HalfEdge -} - -HalfEdge { - otherHalfEdge: HalfEdge - port?: Port -} -``` diff --git a/docs/diary/2024-10-17-maybe-untyped-first.md b/docs/diary/2024-10-17-maybe-untyped-first.md deleted file mode 100644 index df356590..00000000 --- a/docs/diary/2024-10-17-maybe-untyped-first.md +++ /dev/null @@ -1,38 +0,0 @@ ---- -title: maybe untyped first -date: 2024-10-17 ---- - -也许应该先实现无类型的 inet， -这样可以用来自由地观察 inet 这个计算模型的行为， -因为开始的时候，我们还不是真的理解这个计算模型， -所以盲目地给它设计类型系统可能是错误的。 - -按照这个原则，开始的时候也不应该有 port 的 sign 的限制， -即不应该限制只有相反的 sign 的 port 才能相连。 - -可以回到 inet-cute 中做这个修改： - -```inet -node zero value! end -node add1 prev value! end -node add target! addend result end - -rule cons append - (append)-rest (cons)-tail append - (cons)-head cons - result-(append) -end -``` - -# 关于 inet 的类型系统 - -当想要给 inet 加类型系统的时候， -我们想要加 dependent type system， -为了达成这个目标，其实我们不能从「加类型系统」这个角度去看， -而应该从其背后的逻辑系统入手 --- 即从 linear logic 中的谓词演算入手。 - -为什么在考虑「证明的逻辑」时， -会产生 linear logic 这种带有资源语义的系统？ -证明中有什么是和资源相关的？ 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! - - diff --git a/package-lock.json b/package-lock.json index 940629bf..119f39fa 100644 --- a/package-lock.json +++ b/package-lock.json @@ -13,13 +13,13 @@ "@cicada-lang/partech": "^0.2.5", "@xieyuheng/command-line": "^0.1.2", "@xieyuheng/ty": "^0.2.2", - "picocolors": "^1.1.0" + "picocolors": "^1.1.1" }, "bin": { "inet-js": "bin/inet-js" }, "devDependencies": { - "@types/node": "^22.7.5", + "@types/node": "^22.7.7", "@xieyuheng/test-runner": "^0.2.10", "prettier": "^3.3.3", "prettier-plugin-organize-imports": "^4.1.0", @@ -744,9 +744,9 @@ } }, "node_modules/@types/node": { - "version": "22.7.5", - "resolved": "https://registry.npmmirror.com/@types/node/-/node-22.7.5.tgz", - "integrity": "sha512-jML7s2NAzMWc//QSJ1a3prpk78cOPchGvXJsC3C6R6PSMoooztvRVQEz89gmBTBY1SPMaqo5teB4uNHPdetShQ==", + "version": "22.7.7", + "resolved": "https://registry.npmjs.org/@types/node/-/node-22.7.7.tgz", + "integrity": "sha512-SRxCrrg9CL/y54aiMCG3edPKdprgMVGDXjA3gB8UmmBW5TcXzRUYAh8EWzTnSJFAd1rgImPELza+A3bJ+qxz8Q==", "license": "MIT", "dependencies": { "undici-types": "~6.19.2" @@ -1623,9 +1623,9 @@ } }, "node_modules/picocolors": { - "version": "1.1.0", - "resolved": "https://registry.npmmirror.com/picocolors/-/picocolors-1.1.0.tgz", - "integrity": "sha512-TQ92mBOW0l3LeMeyLV6mzy/kWr8lkd/hp3mTg7wYK7zJhuBStmGMBG0BdeDZS/dZx1IukaX6Bk11zcln25o1Aw==", + "version": "1.1.1", + "resolved": "https://registry.npmjs.org/picocolors/-/picocolors-1.1.1.tgz", + "integrity": "sha512-xceH2snhtb5M9liqDsmEw56le376mTZkEX/jEb/RxNFyegNul7eNslCXP9FDj/Lcu0X8KEyMceP2ntpaHrDEVA==", "license": "ISC" }, "node_modules/picomatch": { diff --git a/package.json b/package.json index 194f2919..9bfe0970 100644 --- a/package.json +++ b/package.json @@ -2,6 +2,7 @@ "name": "@cicada-lang/inet-js", "version": "0.3.1", "repository": "github:cicada-lang/inet-js", + "license": "GPL-3.0-or-later", "type": "module", "main": "./lib/index.js", "files": [ @@ -22,20 +23,19 @@ "test": "npm run test:ts && npm run test:inet-run && npm run test:inet-run-error", "format": "prettier src docs --write" }, - "devDependencies": { - "@types/node": "^22.7.5", - "@xieyuheng/test-runner": "^0.2.10", - "prettier": "^3.3.3", - "prettier-plugin-organize-imports": "^4.1.0", - "typescript": "^5.6.3", - "vitest": "^2.1.3" - }, "dependencies": { "@cicada-lang/framework": "^0.2.0", "@cicada-lang/partech": "^0.2.5", "@xieyuheng/command-line": "^0.1.2", "@xieyuheng/ty": "^0.2.2", - "picocolors": "^1.1.0" + "picocolors": "^1.1.1" }, - "license": "GPL-3.0-or-later" + "devDependencies": { + "@types/node": "^22.7.7", + "@xieyuheng/test-runner": "^0.2.10", + "prettier": "^3.3.3", + "prettier-plugin-organize-imports": "^4.1.0", + "typescript": "^5.6.3", + "vitest": "^2.1.3" + } }