December, 2023. Leiden University, Leiden, the Netherlands.

Rust Lambda Calculus

Lambda Calculus Assignment for Leiden University. Free choice of Programming Language.

Assignments

Assignment 1

Grade

10/10

Assignment Instructions

• Lambda Calculus Parser
• Precedence: lambda abstraction groups more strongly than application (i.e. abstraction precedes application), and application associates to the left.
• Grammar: ⟨expr⟩ ::= ⟨var⟩ | '(' ⟨expr⟩ ')' | '' ⟨var⟩ ⟨expr⟩ | ⟨expr⟩ ⟨expr⟩
• See REQUIREMENTS for detailed requirements.

Assignment 2

Grade

10/10

Assignment Instructions

• Lambda Calculus Interpreter (Parser + Reducer)
• Precedence: Lambda abstraction groups more strongly than application (i.e. abstraction precedes application), and application associates to the left.
• Grammar: ⟨expr⟩ ::= ⟨var⟩ | '(' ⟨expr⟩ ')' | '' ⟨var⟩ ⟨expr⟩ | ⟨expr⟩ ⟨expr⟩
• See REQUIREMENTS for detailed requirements.

Assignment 3

Grade

8/10 (Messed up the type checking. Didn't watch the lectures prior to doing Assignment 3, rest is perfect)

• Lambda Calculus Type Checker (Parser + Type Checker)
• Precedence: Lambda abstraction groups more strongly than application (i.e. abstraction precedes application), and application associates to the left.
• Grammar:
  • ⟨judgement⟩ ::= ⟨expr⟩ ':' ⟨type⟩
  • ⟨expr⟩ ::= ⟨lvar⟩ | '(' ⟨expr⟩ ')' | '' ⟨lvar⟩ '^' ⟨type⟩ ⟨expr⟩ | ⟨expr⟩ ⟨expr⟩
  • ⟨type⟩ ::= ⟨uvar⟩ | '(' ⟨type⟩ ')' | ⟨type⟩ '->' ⟨type⟩
    lvar = variable beginning with lowercase latin letter
    uvar = variable beginning with uppercase latin letter
• See REQUIREMENTS for detailed requirements.

Setup

• Install Rust: https://www.rust-lang.org/tools/install
• Rust version used on my machine: 1.74.1 (Not MSRV)

Building & Running

• cd assignment*
  To comply with the assignment requirements:
• make build
  (is equal to cargo build --release)
  (the release flag is important for performance, but not for correctness, removing the flag unleashes some debug macros.)
• Running the program is explained in the assignment folder README.

Cleaning

Just like most Makefiles implement, cargo has a clean command you might want to use: cargo clean
Target folders can get really large, my highest recorded size is 12GB. For simplicity, I added it to the Makefiles, so you can use make clean too.

Some more interesting tools I used

• cargo-watch
  This tool is very useful for development, it watches for changes in the source code and automatically rebuilds the project.

Benchmarking

Benched on a 3.5 GHz 12-Core Intel Xeon E5-2690V3 (24 Threads) with 64GB of DDR4-2133MT RAM. (So definitely room for single-threaded improvement.)

You can repeat these tests by running make run-bench EXPR="a b c" N=1000, make run-bench EXPR="a b c" N=1000000, etc.

Assignment 1

	1 iteration			1,000 iterations			1,000,000 iterations
	Tokenizing	Parsing	Combined	Tokenizing	Parsing	Combined	Tokenizing	Parsing	Combined
a	48ns	49ns	84ns	39µs	46µs	83µs	36ms	46ms	83ms
a b c	95ns	160ns	242ns	80µs	155µs	240µs	80ms	159ms	251ms
(λx((a) (b)))	152ns	381ns	532ns	135µs	305µs	441µs	136ms	307ms	445ms
(λ x a b)	150ns	236ns	362ns	108µs	193µs	302µs	102ms	196ms	304ms
λx.λy.λz.a (λw.b)	248ns	569ns	763ns	215µs	480µs	704µs	214ms	488ms	702ms

Assignment 2

	1,000 iterations				1,000,000 iterations
	Tokenizing	Parsing	Reducing	Combined	Tokenizing	Parsing	Reducing	Combined
(\x y)((\x (x x))(\x (x x)))	338µs	766µs	121µs	1.19ms	287ms	700ms	113ms	1.12s
(\x x x)(\x x x)	203µs	499µs	235µs	926µs	181ms	444ms	221ms	870ms
\t (\x y) t	146µs	308µs	257µs	691µs	130ms	257ms	260ms	660ms
λx.λy.λz.a (λw.b)	241µs	515µs	207µs	951µs	213ms	474ms	214ms	918ms

Assignment 3

	1,000 iterations				1,000,000 iterations
	Tokenizing	Parsing	Type Checking	Combined	Tokenizing	Parsing	Type Checking	Combined
(\x^A (\y^(A->B) (y ((\x^A x) x)))): (A -> ((A -> B) -> B))	716µs	1.47ms	662µs	3.5ms	617ms	1.40s	604ms	3.40s
(\y^A (\x^(A -> (C -> A)) (x y))): (A -> (A -> C -> A) -> C -> A)	669µs	1.33ms	630µs	3.51ms	633ms	1.31s	603ms	3.45s
(\x^A x):(A -> A)	170µs	453µs	280µs	926µs	151ms	418ms	258ms	866ms
(\x^B (\x^A x)):(B -> (A -> A))	286µs	741µs	400µs	1.47ms	261ms	723ms	362ms	1.46s