about to publish

Author: cscccl

Cargo.toml

@@ -0,0 +1,16 @@
+[package]
+name = "lambdascript"
+version = "0.1.0"
+authors = ["Chuck Liang"]
+edition = "2021"
+license = "MIT"
+description = "Educational tool illustrating beta reduction of untyped lambda terms, parser generation"
+repository = "https://github.com/chuckcscccl/lambdascript/"
+keywords = ["lambda-calculus", "lambda", "beta-reduction", "education"]
+categories = ["command-line-utilities", "parsing", "mathematics"]
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+rustlr = "0.2"
+fixedstr = "0.1"
+chrono = "0.4"

README.md

@@ -1,2 +1,91 @@
-# lambdascript
-educational tool illustrating beta reduction of untyped lamba terms, also uses rustlr parser generator
+## Lambdascript
+
+**Lambdascript** executes beta-reduction steps on untyped lambda
+terms.  It is not a high-performance implementation of lambda
+calculus. Rather, the tool serves three primary purposes, all of which
+are illustrational or educational in nature:
+
+  1. It demonstrates the usage of the **[rustlr](https://docs.rs/rustlr/latest/rustlr/index.html)** *parser generator*.  The LALR(1) grammar for lambdascript in rustlr format
+  is given [here](https://cs.hofstra.edu/~cscccl/rustlr_project/lambdascript/untyped.grammar).
+
+  2. For introductory level students in a programming languages class, the
+  tools shows every step of beta reduction, including alpha-conversions where
+  necessary, in reducing a term to normal form.  It includes both full
+  beta-normalization using the normal order (call-by-name) strategy as well as 
+  weak-head normalization using call-by-value.  Definitions can be given
+  for terms such as S, K, I.
+
+  3. For more advanced students, the source code of the program demonstrates
+  how lambda terms can be represented in abstract syntax and how
+  reductions can be implemented.
+
+### Usage
+The program was written in Rust and should be installed as an executable: **`cargo install lambdascript`**. You must have Rust installed (from <https://rust-lang.org>) to execute the cargo command.
+
+The program can read from a script or interactively read from stdin. Expressions and defintions are separated by ; (semicolon).  Here's an example of reading and evaluating from stdin, which can be initiated by running the executable.
+
+```
+<<< (lambda x.x (lambda y.x y)) y;
+(λx.x (λy.x y)) y
+ =>  y (λy1.y y1)
+```
+Lambdascript uses standard syntax for lambda terms: application associates to
+the left and application binds tighter than abstraction, meaning that the
+scope of a λ extends to the right as far as possible unless bounded by
+parentheses.  Lambda expressions inside applications must always by bound
+by parentheses: so `x lambda y.y` should be replaced with `x (lambda y.y)`.
+
+Given a file [simple.ls](https://cs.hofstra.edu/~cscccl/rustlr_project/lambdascript/simple.ls) with the following contents:
+```
+define I = lambda x.x;
+define K = lambda x.lambda y.x;
+define lazy INFINITY = (lambda x.x x) (lambda x.x x);
+
+K I INFINITY x;
+```
+**`lambdascript simple.ls`** produces the following output:
+```
+K I INFINITY x
+= (λxλy.x) I INFINITY x
+ =>  (λy.I) INFINITY x
+= (λyλx.x) INFINITY x
+ =>  (λx.x) x
+ =>  x
+```
+The reduction terminated because normal-order (call-by-name)
+evaluation is applied by default.  If the
+the last line of the file was replaced with `weak (K I INFINITY x)`, then
+weak-head reduction using call-by-value will take place, 
+resulting in an infinite loop.  There will likewise be an infinite loop if
+`lazy` was missing from the definition of `INFINITY`.  Full, normal-order
+evaluation and weak-head call-by-value are the only reduction strategies
+implemented in lambdascript.
+
+After a script is executed, the interpreter automatically enters interactive
+mode with the definitions from the script still available.
+
+The file **[pure.ls](https://cs.hofstra.edu/~cscccl/rustlr_project/lambdascript/pure.ls)** contains a full list of definitions of well-known lambda-calculus
+combinators.
+
+#### Interactive Interpreter Directives
+
+At the `<<<` prompt the following special directives can be given:
+
+  * `exit` or `quit`: exists the program
+  * `use lambda` or `use lam` or `use Lam` or `use \`: On some systems,
+    the Greek character λ (unicode 0x03BB) may fail to display properly.
+    To change the symbol displayed for lambda, you can choose between one
+    of four alternatives (the choices are limited to these four because the
+    symbol must be a statically allocated string).
+  * `use greek` or `use unicode`: reverts to displaying λ, which is the default
+  * `trace off`: turns off the displaying of intermediate reduction steps: only the initial term and the final normal form are shown
+  * `trace medium`: Beta-reduction steps are shown, but not the expansion
+    of defintions nor alpha-conversion
+  * `trace on` or `trace max`: restore displaying of all steps: this is the
+    default
+
+-----------------------------
+
+As this tool is used actively in the classroom, each release will have
+a **limited lifetime**: after a certain period it will cease to work until
+a new version is released.

combinators.ls

@@ -0,0 +1,52 @@
+// Programming with pure lambda terms, with full beta and weak head reduction
+// default define means reduce defined term to weak-head normal form.
+
+define I = lambda x.x;
+define K = lambda x.lambda y.x;
+define S = lambda x.lambda y.lambda z.(x z (y z));
+define True = K;
+define False = (K I);
+define IF = lambda b.lambda x.lambda y.(b x y);
+define NOT = lambda b.(IF b False True);
+define OR = lambda a.lambda b.(IF a True b);
+define AND = lambda a.lambda b.(IF a b False);
+define CONS = lambda a.lambda b.lambda c.(IF c a b);
+define CAR = lambda c.(c True);
+define CDR = lambda c.(c False);
+define lazy FIX = lambda M.((lambda x.(M (x x))) (lambda y.(M (y y))));
+define Zero = False;
+define One = lambda f.lambda x.(f x);
+define PLUS = lambda m.lambda n.lambda f.lambda x.(m f (n f x));
+define TIMES = lambda m.lambda n.lambda f.lambda x.(m (n f) x);
+//define lazy INFINITY = (lambda x.(x x)) (lambda x.(x x));
+
+define NULL = False;
+define M = (CONS 2 (CONS 3 (CONS 5 (CONS 7 NULL))));
+
+(K 1);     // lambda y.1
+(K 1 2);   // 1
+(K I);     // lambda x.lambda y.y
+(K I 2);   // lambda y.y
+(K I 2 3); // 3
+//weak (S K I); // weak head normal form
+(S K I);   // full normal form
+(S K I I); // lambda x.x
+(S K I 0); // 0
+
+// booleans and if-else
+(IF (AND (NOT False) True) 1 2);  // 1
+
+// linked lists:
+(CAR (CDR (CDR M)));  // 5
+
+// arithmetic
+(PLUS One One);  // 2 in church numeral
+
+(TIMES (PLUS One One) Zero 1 0); // 0: 2*0=0!
+
+// static scoping: 
+let x = 1 in 
+  (let f = lambda y.x in 
+    (let x = 2 in (f 0)));  // 1, since lambda calc implies static scoping.
+                            // if 2 was printed, then it's dynamically scoped
+			    // and something went horribly wrong.

hw1.ls

@@ -0,0 +1,93 @@
+// Sample Solutions to Lambda Calculus Homework in Lambdascript.
+
+// 2.
+2;  // 2 is evaluated into 2, which is already a normal form
+(lambda x.lambda y. (y x)) u (lambda x.x);
+
+
+// 3. Basic combinators:
+3;
+define I = lambda x.x;
+define K = lambda x.lambda y.x;
+define S = lambda x.lambda y.lambda z.x z (y z);
+
+K I I;
+S I K;
+S K (K I);
+S (K I);
+
+// note that the lambdascript program does call-by-name by default.
+weak (S (K I));  // this does "weak head reduction using call-by-value"
+
+// 4. Arithmetic
+4;
+define ZERO = K I;
+define ONE = lambda f.lambda x.f x;
+define PLUS = lambda m.lambda n.lambda f.lambda x.m f (n f x);
+define TIMES = lambda m.lambda n.lambda f.lambda x.m (n f) x;
+define TWO = PLUS ONE ONE;
+
+PLUS TWO ONE;
+TIMES ZERO TWO;
+
+// 4b.
+4 b;  // a space is needed otherwise there's parser error
+define EXPT = lambda m.lambda n.n m;
+define TREE = PLUS ONE TWO;
+
+EXPT TREE TWO;
+
+
+// 5. Booleans and if-else
+5;
+define TRUE = K;     // K A B = A
+define FALSE = K I;  // (K I) A B = B
+define IF = lambda b.lambda x.lambda y.b x y;
+define NOT = lambda b.IF b FALSE TRUE;
+define OR = lambda a.lambda b.IF a TRUE b;
+define AND = lambda a.lambda b.IF a b FALSE;
+OR;
+OR FALSE FALSE;
+OR FALSE TRUE;
+OR TRUE FALSE;
+OR TRUE TRUE;
+
+
+6;
+define NOT = lambda n.n FALSE TRUE;
+NOT;
+NOT FALSE;
+NOT TRUE;
+NOT (NOT TRUE);  // "no, no it can't be true!"  but it is.
+
+7;
+IF TRUE 1 2;
+IF FALSE 1 2;
+
+
+// Data structure (pairs, linked-list = nested pairs)
+define PAIR = lambda a.lambda b.lambda c.IF c a b; // called "CONS"
+define FST = lambda c.c TRUE;  // first element of cons pair, "CAR"
+define SND = lambda c.c FALSE; // second element of cons pair, "CDR"
+define NIL = FALSE;   // represents empty list
+define ISNIL = lambda p.p (lambda a.lambda b.lambda z.FALSE) TRUE;
+
+8;
+define M = PAIR a (PAIR b c);
+M;
+FST M;
+SND M;
+SND (SND M);
+
+9;
+define ISZERO = lambda n.n (lambda z.FALSE) TRUE;
+ISZERO;
+ISZERO (TIMES ONE ZERO);
+ISZERO (PLUS ONE ZERO);
+
+10;
+still working on it;
+define lazy INFINITY = (lambda x.x x) (lambda x.x x);
+// without "lazy" it will go into an infinite loop
+
+//  weak (INFINITY);   // uncomment at your own risk...

pure.ls

@@ -0,0 +1,97 @@
+// Programming with pure lambda terms, with full beta-normalization via CBN.
+
+// Baisc combinators:
+define I = lambda x.x;
+define K = lambda x.lambda y.x;
+define S = lambda x.lambda y.lambda z.x z (y z);
+
+// Booleans and if-else
+define TRUE = lambda x.lambda y.x;     // K A B = A
+define FALSE = lambda x.lambda y.y;  // (K I) A B = B
+define IF = lambda b.lambda x.lambda y.b x y;
+define NOT = lambda b.IF b FALSE TRUE;
+define OR = lambda a.lambda b.IF a TRUE b;
+define AND = lambda a.lambda b.IF a b FALSE;
+
+// Arithmetic
+define ZERO = lambda f.lambda x.x;
+define ISZERO = lambda n.n (lambda z.FALSE) TRUE;
+define ONE = lambda f.lambda x.f x;
+define PLUS = lambda m.lambda n.lambda f.lambda x.m f (n f x);
+define TIMES = lambda m.lambda n.lambda f.lambda x.m (n f) x;
+define PRED = lambda n.lambda f.lambda x.n (lambda g.lambda h.h (g f)) (lambda u.x) (lambda u.u);
+define SUBTRACT = lambda m.lambda n. n PRED m;
+define LEQ = lambda m.lambda n. ISZERO (SUBTRACT m n);  // <=
+define EQUALS = lambda m.lambda n.AND (LEQ m n) (LEQ n m);
+LEQ ONE (PLUS ONE ONE);   //true
+LEQ (PLUS ONE ONE) ONE;  // false
+EQUALS ONE (TIMES ONE ONE); // true
+
+// Data structure (pairs, linked-list = nested pairs)
+define CONS = lambda a.lambda b.lambda c.IF c a b; //pair constructor
+define CAR = lambda c.c TRUE;  // first element of cons pair
+define CDR = lambda c.c FALSE; // second element of cons pair
+define NIL = FALSE;   // represents empty list
+define ISNIL = lambda p.p (lambda a.lambda b.lambda z.FALSE) TRUE;
+
+// Recursion (loops) and divergence.
+define lazy INFINITY = (lambda x.(x x)) (lambda x.(x x));
+define lazy FIX = lambda m.(lambda x.m (x x)) (lambda y.m (y y));
+
+// A sample linked list
+define TWO = PLUS ONE ONE;
+define THREE = PLUS TWO ONE;
+define FIVE = PLUS TWO THREE;
+define P = (CONS TWO (CONS THREE (CONS FIVE NIL)));
+
+SUBTRACT FIVE THREE;
+
+I 1;
+K 1;     // lambda y.1
+K 1 2;   // 1
+K I;     // lambda x.lambda y.y
+K I 2;   // lambda y.y
+K I 2 3; // 3
+S K I;   
+S I I;
+
+IF (AND (NOT FALSE) TRUE) 1 2;  // 1
+
+// linked lists:
+CAR (CDR (CDR P));  // 5  // in oop languages, M.cdr().cdr().car()
+ISNIL NIL;
+ISNIL P;
+
+// recursive function to sum all numbers in list L:
+define lazy SUM = FIX (lambda f.lambda L. IF (ISNIL L) ZERO (PLUS (CAR L) (f (CDR L))));
+
+//SUM P;  // reduces to church numeral 10 (do in interactive mode)
+
+TIMES (PLUS ONE ONE) ZERO; // 2*0=0, 0 in church numeral is lambda f.lambda x.x
+
+let x = ONE in (PLUS x x); // 2 in church numeral
+// the above is expanded by the parser to ((lambda x.PLUS x x) ONE)
+
+// static scoping: 
+let x = 1 in 
+  (let f = lambda y.x in 
+    (let x = 2 in (f 0)));  // 1, since lambda calc implies static scoping.
+                            // if 2 was printed, then it's dynamically scoped
+			    // and something went horribly wrong.
+/* the above let-expression expands to:
+(λx.(λf.(λx.f 0) 2) (λy.x)) 1
+ =>  (λf.(λx.f 0) 2) (λy.1)
+ =>  (λx.(λy.1) 0) 2
+ =>  (λy.1) 0
+ =>  1
+
+lambda calculus version of C program:
+int x = 1;
+int f(int y) { return x; }
+int main()  {
+  int x = 2;
+  return f(0);
+} // main returns 1 under static scoping, 2 under dynamic scoping.
+
+C and virtually all languages are statically scoped.
+*/

simple.ls

@@ -0,0 +1,5 @@
+define I = lambda x.x;
+define K = lambda x.lambda y.x;
+define lazy INFINITY = (lambda x.x x) (lambda x.x x);
+
+K I INFINITY x;