victortaelin / interaction-calculus Goto Github PK
View Code? Open in Web Editor NEWA programming language and model of computation that matches the optimal λ-calculus reduction algorithm perfectly.
License: MIT License
A programming language and model of computation that matches the optimal λ-calculus reduction algorithm perfectly.
License: MIT License
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?
The readme mentions
I've read the blogpost and the linked paper but were not able to find specifics about this. The reason I ask is because I'd love to visualize programs in the combinator form to build intuition. Can you clarify?
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. :-)
Is there an implementation of amb agent for representing non-deterministic computations?
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?
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?
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.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.