Giter VIP home page Giter VIP logo

interaction-calculus's Issues

Error in rewrite implementation

In net::rewrite, when kinds are the same, x slot 1 is linked to y slot 1 and x slot 2 is linked to y slot 2. Shouldn't this be the other way round for symmetric interaction combinators? So x1 <-> y2 and x2 <-> y1?

benchmarks for comparison

I think it will grate if there is a list of benchmarks to show the advantage compared to existing languages/platforms, such as Solidity/EVM, Haskell, etc. For example, some parallel example that cannot be easily implemented in blockchain because it is hard to eliminate non-deterministic behaviour caused by data race.

The paper https://medium.com/@maiavictor/the-abstract-calculus-fe8c46bcf39c is very good, but simple examples can be more intuitive and be more convincible. Some simple examples will be easier for me to convince my boss. :-)

Naming

If anyone has a suggestion for a better name (since Abstract Calculus seems to be impopular) please let me know. Symmetric Lambda Calculus (since it is isomorphic to Symmetric Interaction Combinators) may be a good option. Thoughts?

Example stackoverflow

I modified the project a little bit to run example.rs with cargo test:

diff --git a/src/example.rs b/src/example.rs
index 85ff15f..bbcaaeb 100644
--- a/src/example.rs
+++ b/src/example.rs
@@ -7,8 +7,7 @@
 // - [-] stands for an erased (unused) lambda or let variable
 // - [/a b c] inlines all occurrences of [a] by the closed term [b]

-mod term;
-mod net;
+use term;

 pub fn example() {
     let example = term::from_string(b"
diff --git a/src/main.rs b/src/main.rs
index d518a19..5387cda 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -4,6 +4,7 @@ use clap::{Arg, App};
 mod term;
 mod net;
 mod extra;
+mod example;

 use term::*;
 use extra::*;
@@ -104,3 +105,12 @@ fn main() -> io::Result<()> {

     Ok(())
 }
+
+mod tests {
+    use super::example::*;
+
+    #[test]
+    fn test_example() {
+        example();
+    }
+}

After that, I did cargo test and it gives me

thread 'tests::test_example' has overflowed its stack
error: test failed, to rerun pass '--bin sic'

Is example.rs a working example?

Some programs make it hang/loop forever

This program makes it hang forever:

def Z = λs λz (z)
def S = λn λs λz dup #s s1 s2 = s; (s1 (n s2 z))
def pow = λa λb (b a)
(pow (S (S Z)) (S (S Z)))

I added a println!("{}", from_net(&inet)); after the call to rewrite, then it prints:

dup #s e f = c; dup #s j k = h; dup #s p q = n; dup #s u v = s; (λa (a (λb λc λd (e ((b f) d)) (λg λh λi (j ((g k) i)) λ* λl l))) (λm λn λo (p ((m q) o)) (λr λs λt (u ((r v) t)) λ* λw w)))
dup #s d e = b; dup #s i j = g; dup #s o p = m; dup #s t u = r; ((λa λb λc (d ((a e) c)) (λf λg λh (i ((f j) h)) λ* λk k)) (λl λm λn (o ((l p) n)) (λq λr λs (t ((q u) s)) λ* λv v)))
dup #s c j = a; dup #s g h = e; dup #s n o = l; dup #s s t = q; (λa λb (c (((λd λe λf (g ((d h) f)) λ* λi i) j) b)) (λk λl λm (n ((k o) m)) (λp λq λr (s ((p t) r)) λ* λu u)))
dup #s m n = k; dup #s r s = p; dup #s b i = (λj λk λl (m ((j n) l)) (λo λp λq (r ((o s) q)) λ* λt t)); dup #s f g = d; λa (b (((λc λd λe (f ((c g) e)) λ* λh h) i) a))
dup #s l s = j; dup #s p q = n; dup #s b i = λj λk (l (((λm λn λo (p ((m q) o)) λ* λr r) s) k)); dup #s f g = d; λa (b (((λc λd λe (f ((c g) e)) λ* λh h) i) a))
dup #s m t = [b j#s]; dup #s q r = o; dup #s c k = λl (m (((λn λo λp (q ((n r) p)) λ* λs s) t) l)); dup #s g h = e; λa (λb c (((λd λe λf (g ((d h) f)) λ* λi i) λj k) a))
dup #s p q = n; dup #s d k = [(((λm λn λo (p ((m q) o)) λ* λr r) λs l) a) s#s]; dup #s h i = f; dup #s b l = λc (d (((λe λf λg (h ((e i) g)) λ* λj j) k) c)); λa b
dup #s q r = o; dup #s d k = [(((λn λo λp (q ((n r) p)) λ* λs s) λt λl m) a) t#s]; dup #s h i = f; dup #s c m = (d (((λe λf λg (h ((e i) g)) λ* λj j) k) [b l#s])); λa λb c
dup #s g h = e; dup #s p q = n; dup #s c l = ((((λd λe λf (g ((d h) f)) λ* λi i) λj λk l) a) (((λm λn λo (p ((m q) o)) λ* λr r) j) [b k#s])); λa λb c
dup #s f h = d; dup #s o p = m; dup #s c k = (((λd λe (f ((λ* λg g h) e)) λi λj k) a) (((λl λm λn (o ((l p) n)) λ* λq q) i) [b j#s])); λa λb c
dup #s e g = λn λo p; dup #s k l = i; dup #s c p = ((λd (e ((λ* λf f g) d)) a) (((λh λi λj (k ((h l) j)) λ* λm m) n) [b o#s])); λa λb c
dup #s d f = λm λn o; dup #s j k = h; dup #s c o = ((d ((λ* λe e f) a)) (((λg λh λi (j ((g k) i)) λ* λl l) m) [b n#s])); λa λb c
dup #s e h = λo p; dup #s l m = j; dup #s c p = ((λd e ((λ* λf f λg h) a)) (((λi λj λk (l ((i m) k)) λ* λn n) [d g#s]) [b o#s])); λa λb c
dup #s d m = λn o; dup #s h i = f; dup #s c o = (d (((λe λf λg (h ((e i) g)) λ* λj j) [((λ* λk k λl m) a) l#s]) [b n#s])); λa λb c
dup #s e o = p; dup #s i j = g; dup #s c p = (λd e (((λf λg λh (i ((f j) h)) λ* λk k) [((λ* λl l λm λn o) a) m#s]) [b [d n#s]#s])); λa λb c
dup #s d f = e; dup #s c e = d; λa λb c

For better readability I also ran it with lazy-REF nodes, then it prints:

(λa (a (S (S Z))) (S (S Z)))
((S (S Z)) (S (S Z)))
dup #s c d = a; (λa λb (c (((S Z) d) b)) (S (S Z)))
dup #s b c = (S (S Z)); λa (b (((S Z) c) a))
dup #s f g = d; dup #s b c = λd λe (f (((S Z) g) e)); λa (b (((S Z) c) a))
dup #s g h = [b d#s]; dup #s c e = λf (g (((S Z) h) f)); λa (λb c (((S Z) λd e) a))
dup #s d e = [(((S Z) λg f) a) g#s]; dup #s b f = λc (d (((S Z) e) c)); λa b
dup #s d e = [(((S Z) λh λf g) a) h#s]; dup #s c g = (d (((S Z) e) [b f#s])); λa λb c
dup #s c f = ((((S Z) λd λe f) a) (((S Z) d) [b e#s])); λa λb c
dup #s f g = d; dup #s c j = (((λd λe (f ((Z g) e)) λh λi j) a) (((S Z) h) [b i#s])); λa λb c
dup #s e f = λg λh i; dup #s c i = ((λd (e ((Z f) d)) a) (((S Z) g) [b h#s])); λa λb c
dup #s d e = λf λg h; dup #s c h = ((d ((Z e) a)) (((S Z) f) [b g#s])); λa λb c
dup #s e g = λh i; dup #s c i = ((λd e ((Z λf g) a)) (((S Z) [d f#s]) [b h#s])); λa λb c
dup #s d f = λg h; dup #s c h = (d (((S Z) [((Z λe f) a) e#s]) [b g#s])); λa λb c
dup #s e h = i; dup #s c i = (λd e (((S Z) [((Z λf λg h) a) f#s]) [b [d g#s]#s])); λa λb c
dup #s d f = e; dup #s c e = d; λa λb c

The dup label #s is reused between S calls but shouldn't be.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.