Lambda Calculus Parser
This is a parser for λ-calculus expressions. It takes a λ-terms as input, parses it and returns a JSON representation of the term. The parser currently supports λ-abstractions, variables and function applications. It uses a recursive descent parsing technique.
Features
- Parses λ-abstractions, variables and function applications
- Returns a JSON representation of the parsed λ-term
- Includes a REPL for interactive parsing
Usage
The parser is implemented as a Parser struct with several methods. It uses a Peekable<Chars> iterator to read the input string single characters at a time. The main parsing function, parse_term, loop over the input string and determine the appropriate parsing function to call based on the current character.
The parsing functions are:
parse_lambda: Parsed a λ-abstraction(e.g.,λx.x)parse_application: Parses a function application (e.g.,(f x))parse_variable: Parses a variable (e.g.,x)
The parser returns an enum Term, which can be one of the following:
Lambda: Represents a λ-abstraction with a binding variable and a bodyApplication: Represents a function application with a function and an argumentVariable: Represents a variable with a nameNull: Represents an empty term or failed parsing
The parsed Term is then converted to a JSON format using the term_to_json function. which converts the Term to a serde_json::Value object.
Example
Here's an example of how to parse a λ-term using the parser:
fn main() {
let input = "λf. λx. (f x)";
let term = parse(input);
let json = term_to_json(&term);
println!("{}", serde_json::to_string_pretty(&json).unwrap());
}
This will output:
{
"bind": "f",
"body": {
"bind": "x",
"body": {
"arg": {
"name": "x",
"tag": "var"
},
"func": {
"name": "f",
"tag": "var"
},
"tag": "application"
},
"tag": "lambda"
},
"tag": "lambda"
}
Note: There is a problem that the position of the tag goes down when print the current JSON. This will be fixed in the future.
To use the REPL, run the following command:
cargo run
After that, you can enter a λ-term and press enter to parse it. The REPL will print the parsed JSON representation of the term.
16 Aug 23, 2022
5 Feb 1, 2022
3 Dec 29, 2022
2 Mar 19, 2022
4 May 25, 2022
18 Jan 2, 2023
7 Jan 18, 2023
34 Sep 13, 2022
8 Dec 15, 2022
18 Oct 18, 2022
10 Dec 8, 2022
1 Apr 3, 2022
14 Jan 7, 2023
255 Dec 30, 2022
2k Jan 3, 2023
54 Dec 23, 2022
598 Jan 2, 2023
314 Dec 18, 2022
793 Jan 2, 2023