### 2 releases

0.3.1 | Mar 20, 2024 |
---|---|

0.3.0 | Jan 26, 2024 |

#**93** in Value formatting

**55** downloads per month

**MIT**license

52KB

1K
SLoC

# Lambda Shell

This is a simple REPL shell for untyped lambda expressions. I wrote it mostly for playing around a little bit with the lambda calculus. Some parts of it are wildly inefficient, but it is fine for education purposes.

The shell can evaluate lambda expressions, assignments and macros.

# Example

There are builtin terms

and `SUCC`

to create natural numbers using church numerals:`NIL`

`[`λ`]` `@`usestd
`@`usestd
`[`λ`]` one `:``=` `SUCC` `NIL`
one `:``=` `SUCC` `NIL`
`[`λ`]` two `:``=` `SUCC` `(``SUCC` `NIL``)`
two `:``=` `SUCC` `(``SUCC` `NIL``)`
`[`λ`]` `!`normalize `(``ADD` one two`)`
\f `.` \x `.` f `(`f `(`f x`)``)`

You can select different reduction strategies at runtime:

`[`λ`]` `@`usestd
`@`usestd
`[`λ`]` `!`vnormalize `(``AND` `TRUE` `FALSE``)`
`AND` `TRUE` `FALSE`
`(`\q `.` `TRUE` q `TRUE``)` `FALSE`
`(`\q `.` `(`\y `.` q`)` `TRUE``)` `FALSE`
`(`\q `.` q`)` `FALSE`
`FALSE`
`[`λ`]` `@`set strategy normal
`@`set strategy normal
`[`λ`]` `!`vnormalize `(``AND` `TRUE` `FALSE``)`
`AND` `TRUE` `FALSE`
`(`\q `.` `TRUE` q `TRUE``)` `FALSE`
`TRUE` `FALSE` `TRUE`
`(`\y `.` `FALSE``)` `TRUE`
`FALSE`

## Features

- normal (leftmost-outermost) and applicative (leftmost-innermost) reduction strategies
- capture-avoiding substitution
- simple constructs provided via builtins
- macros for processing lambda terms

## Installation

You can find more information about installation and building from source here.

#### Dependencies

~8–21MB

~274K SLoC