0.2.3 • Public • Published

Lambda Calculus

More restraint and more pure,
so functional and so reduced.

-- Anonymous Bauhaus Student

An implementation of (Untyped) Lambda Calculus.

• Use S-expression as overall syntax, to expression ideas clearly.
• Implement call-by-need lazy evaluation.
• Allow recursive in top-level definitions.
• No mutual recursion, a name must be defined before used.
• A simple module system with only one API -- `(import)`.
• It can import module from local file or remote URL.
• Two simple testing statements `(assert-equal)` and `(assert-not-equal)`.
• They can handle beta and eta equivalence.

Usages

Command line tool

Install it by the following command:

`npm install -g @cicada-lang/lambda`

The command-line program is called `lambda`.

open a REPL:

`lambda repl`

or just:

`lambda`

Run a file:

`lambda run tests/nat-church.md`

Run a file and watch file change:

`lambda run tests/nat-church.md --watch`

Examples

Please see tests for more examples.

Boolean

```(define (true t f) t)
(define (false t f) f)

(define (if p t f) (p t f))

(define (and x y) (if x y false))
(define (or x y) (if x true y))
(define (not x) (if x false true))

(and true false)
(not (not (or true false)))```

Natural Number by Church encoding

```(define zero (lambda (base step) base))
(define (add1 n) (lambda (base step) (step (n base step))))
(define (iter-Nat n base step) (n base step))

Factorial

```(import "./nat-church.md"
zero one two three four)

(import "./boolean.md"
true false if)

(define (factorial n)
(if (zero? n)
one
(mul n (factorial (sub1 n)))))

(factorial zero)
(factorial one)
(factorial two)
(factorial three)```

Factorial by fixpoint combinator

```(import "./nat-church.md"
zero one two three four)

(import "./boolean.md"
true false if)

;; NOTE `x` is `f`'s fixpoint if `(f x) = x`
;;   In lambda calculus, we have function `Y`
;;   which can find fixpoint of any function.
;;      (f (Y f)) = (Y f)

(define (Y f)
((lambda (x) (f (x x)))
(lambda (x) (f (x x)))))

;; (claim factorial-wrap (-> (-> Nat Nat) (-> Nat Nat)))
;; (claim (Y factorial-wrap) (-> Nat Nat))
;; (claim y (forall (A) (-> (-> A A) A)))

(define (factorial-wrap factorial)
(lambda (n)
(if (zero? n)
one
(mul n (factorial (sub1 n))))))

(define factorial (Y factorial-wrap))

(factorial zero)
(factorial one)
(factorial two)
(factorial three)
(factorial four)```

Cons the Magnificent

```;; NOTE Temporarily save `car` and `cdr` to a lambda,
;;   apply this lambda to a function -- `f`,
;;   will apply `f` to the saved `car` and `cdr`
(define (cons car cdr) (lambda (f) (f car cdr)))
(define (car pair) (pair (lambda (car cdr) car)))
(define (cdr pair) (pair (lambda (car cdr) cdr)))

(import "./boolean.md"
true false)

(define (null f) true)
(define (null? pair) (pair (lambda (car cdr) false)))

(null? null)```

Development

```npm install           # Install dependencies
npm run build         # Compile `src/` to `lib/`
npm run build:watch   # Watch the compilation
npm run format        # Format the code
npm run test          # Run test
npm run test:watch    # Watch the testing```

Contributions

To make a contribution, fork this project and create a pull request.

Remember to add yourself to AUTHORS. Your line belongs to you, you can write a little introduction to yourself but not too long.

GPLv3

none

Package Sidebar

Install

`npm i @cicada-lang/lambda`

101

0.2.3

GPL-3.0-or-later

254 kB

434