lamcal-repl is a Lambda Calculus REPL command line application written in Rust. It can be used to play around with lambda calculus expressions interactively.
This application is inspired by this talk by glebec where he plays around with lambda calculus in a JavaScript console.
lamcal-repl uses the lamcal library crate for the lambda calculus functionality and adds
the REPL things to make it an application. The name of the executable is lamcali.
To install the lamcal-repl command line application run the following commands in your terminal:
> cargo install lamcal-repl
After it has been installed successfully we can run lamcal-repl by typing the name of the executable:
> lamcali
Alternatively we can clone this git repository, go to the repl subdirectory and type cargo run,
like so
> cd lamcal/repl
lamcal/repl> cargo run
When the application starts we see the following in the command line:
info: Welcome to lamcal-repl, the Lambda Calculus REPL, version 0.4.0
λ>
Notice that the command line prompt changes to λ>. To evaluate a lambda expression we simple type
in the expression at the prompt, like so:
λ> (\x.(\y.x y) a) b
After pressing enter, the expression gets parsed and the default α-conversion and β-reduction is applied. The result is printed to the console, like so:
λ> (\x.(\y.x y) a) b
b a
We can use the backslash character \ or the greek lowercase lambda λ to denote a lambda abstraction with a lambda expressions. The parser understands both backslash as well as the lowercase lambda symbol as the start of an abstraction.
The repl support commands to control the behavior of the application. Commands always start with a colon. Most important commands are:
:hor:helpto print out help information:qor:quitto quit the application
A list of all implemented commands is given in the help information (command :h).
When playing around with more complex expressions typing them can be tedious. Therefore the lamcal
crate provides the possibility to evaluate terms in an environment with predefined terms bound to
names. During evaluation free variables with a name that is bound to a term in the environment is
replaced by the bound term. On startup of the REPL it instantiates a default environment as the
global environment. The global environment is used when evaluating expression by default.
To add new bindings to the environment or replace existing ones we use the :let command. For
example the following command binds the name rev to the term λf.λa.λb.f b a
λ> :let rev = λf.λa.λb.f b a
Now when we use rev as a free variable in any expression it will be replaced by the whole
expression to the right side of the equal sign.
λ> rev
λf.λa.λb.f b a
λ> rev f x y
f y x
The last evaluation is equal to typing:
λ> (λf.λa.λb.f b a) f x y
f y x
If we want to perform a beta-reduction without expanding bound names we can use the :b command
like so:
λ> :b (λa.rev a) f x y
rev f x y
To expand bound names without reducing the term we can use the :x command:
λ> :x (λa.rev a) f x y
(λa.(λf.λa.λb.f b a) a) f x y
In inspected mode we can follow every single step of expansion and reduction. To switch on the
inspected mode we type the command :i.
λ> :i
Inspected mode switched on
When we now evaluate an expression we get the intermediate results of every single step printed to the terminal:
λ> I x
I x
(λa.a) x
x
First I is expanded to the identity term (λa.a) and then it is applied to the variable x which
gives as the result of x. Cool! Isn't it? To switch off the inspected mode we just type the
command :i again.
The following commands are available:
:h or :help displays this help information
:q or :quit quits the repl session
:v or :version prints out the version of lamcali
:i or :inspected toggle inspected mode on and off. In inspected mode the
result of each step during evaluation or reduction is
printed to the terminal.
:e <expr> or :eval <expr>
evaluates the lambda expression <expr>. This command is
equivalent to just typing a lambda expression and
pressing [enter].
:b <expr> or :beta <expr>
performs a beta-reduction on the lambda expression <expr>
using the current set strategy.
:x <expr> or :expand <expr>
replaces free variables in the lambda expression <expr>
with the expression bound to the variable's name in the
current environment.
:p <expr> or :parse <expr>
parses the lambda expression <expr> and prints out the
abstract syntax tree (AST) of the lambda expression.
:bs or :beta-strategy
prints the current set beta-reduction strategy.
:bs <strategy> or :beta_strategy <strategy>
set the beta-reduction strategy to <strategy>.
<strategy> can be one of:
app : applicative-order reducing to normal form
cbn : call-by-name reducing to weak head normal form
cbv : call-by-value reducing to weak normal form
hap : hybrid-applicative-order reducing to normal form
hno : hybrid-normal-order reducing to normal form
hsp : head-spine reducing to head normal form
nor : normal-order reducing to normal form (the default)
:as or :alpha-strategy
prints the current set alpha-conversion strategy.
:as <strategy> or :alpha-strategy <strategy>
set the alpha-conversion strategy to <strategy>.
<strategy> can be one of:
enumerate : appending increasing digits (the default)
prime : appending tick symbols
:let <name> = <expr>
defines a new binding of <expr> to <name> and adds it to
the environment. If a binding with the same name
previously existed in the environment it is replaced by
the new binding.
:clr-env clears the environment, all bindings are removed
:ld-env default loads the default set of predefined bindings into the
environment. Existing bindings with the same name as a
binding in the default set will be replaced. Existing
bindings with no name clash will not be changed.
:ls-env lists all bindings defined in the environment
:ls-env <pattern> lists all bindings filtered by <pattern>. It lists all
bindings with a name that contains the given pattern as a
substring (ignoring case).
Licensed under Apache License, Version 2.0
see LICENSE or http://www.apache.org/licenses/LICENSE-2.0 for details.
Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be licensed as above, without any additional terms or conditions.