An interpreter for λ-calculus implemented in ruby, as part of our course project CS350A: Principles of Programming Languages under Prof. Satyadev Nandakumar, in Fall Semester 2022-23, IIT Kanpur.
The grammar specification is:
λ − term ::= variable |
(\variable · λ − term) |
[λ − term][λ − term]
The allowed variables are single lowercase English letters - a, b, c etc.
It supports the following features:
- Lexer and grammar checker for lambda term expression using LL(1) parser
- Determine free variables in given lambda term
- Free variables substitution
- Alpha Renaming and Beta Reduction
.
├── assets/
├── lexer.rb
├── LICENSE
├── main.rb
├── parser.rb
├── README.md
├── reducer.rb
├── tests/
└── utils.rb
2 directories, 14 filesKeep your λ-expression in a file and pass its filepath as an argument to main.rb.
Lambda Calculus Interpreter
===========================
Usage: main.rb [options]
-i, --input FILE Input file containing λ-expression
-o, --output FILE (Optional) Output file to store reduced λ-expression. Default: out.txtNote that we use the notation of v{i}, where i := [1,2,3,...] for our bound variables after the processing of alpha-renaming and beta-reduction. This helps in easily identifying the bound variables and keep their count in the final reduced form.
$ ruby main.rb -i tests/9.lc ## or
$ ruby main.rb --input=tests/9.lc
================
Course Project
Lambda Calculus Interpreter
Created by: Ayush, Gurbaaz and Kritin
================
Grammar checker :-
[ ( \ x . x ) ] [ y ] is a valid lambda term
================
Free variables :- y
================
α-renaming :- [ ( \ v0 . v0 ) ] [ y ]
================
> Please provide the free variable name along with its substitution. e.g. x:=M denotes replacing free occurences of x with lambda term M
> or press ENTER to finish
y:=(\x.x)
Free variable substitution :- [ ( \ v1 . v1 ) ] [ ( \ v2 . v2 ) ]
================
> All free variables have been substituted successfully! (Closed Form)
Exiting...
================
β-reduction :-
Step 1. ( \ v2 . v2 )
No further reduction possible!
================
Final β-reduced form '( \ v2 . v2 )' saved to 'out.txt'
================You may find some of the lambda expression files in tests/ directory.
 Ayush Kumar |
 Gurbaaz Singh Nandra |
Kritin Sharma |