Lamcal REPL

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.

Installation

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

Usage

When the application starts we see the following in the command line:

info: Welcome to lamcal-repl, the Lambda Calculus REPL, version 0.3.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:

• :h or :help to print out help information
• :q or :quit to quit the application

A list of all implemented commands is given in the help information (command :h).

let bindings and the environment

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

inspected mode

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.

Commands

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).

License

Licensed under Apache License, Version 2.0 see LICENSE or http://www.apache.org/licenses/LICENSE-2.0 for details.

Contribution

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.