λ-X

This project seeks to explore many different fields associated with functional programming and alternative methods of computation. It uses a lambda calculus abstract syntax, and lambda calculus parser written in Haskell. This lambda calculus abstract syntax and parser is used as a bridge to define the lambda calculus in the lambda calculus. Haskell is our bootstrap. On top of this the SECD virtual machine architecture will be implemented in Haskell, allowing us to compile our lambda calculus implementation into to SECD instruction set, where lambda calculus programs will be runnable.

Lambda Calculus Parser (dot-lam) ← Written in Haskell

Concrete Syntax:

module → 'module' alpha '\n'
import → 'import' alpha '\n'
alias → lower '=' expression ';'
expression → expression expression | abstraction | variable | constant | reduction
abstraction → 'L' lower '.' expression
variable → lower
constant → '#'lower
lower → (any series of lowercase characters)
alpha → (any series of alphabetic characters)

Lambda Expression Encoder ← Written in Haskell

Encodes lambda terms to a numerical representation, allowing a lambda expression to evaluate the lambda calculus. This is a requirement, because of the Lambda Calculus's syntactic purity there is no way to perform beta reduction without syntactically distinct representations for both variables and lambda constructs (applications, abstractions, and variables). Church-Numerals provide syntactically distinct elements for an lambda expressions to compare and test against.

The following relation is used to translate a lambda expression (as a Haskell data type) to list of Church-Numerals representing the expression.

App → \f.\x. f (f x) → 2
Lam → \f.\x. f x → 1
Var → \f.\x. x → 0

Variable names are translated to Church-Numerals as well, and begin with 0. Expressions are encoded as a list would be in the Lambda Calculus.

Example:
\a.\b. a b would be encoded to (1,(0,(1,(1,(2,(0,1))))))

Lambda Calculus Core ← Lambda Calculus

The Core is collection of Lambda Calculus functions. These functions are used to write a function which takes an encoded Lambda Calculus expression and evaluates it.

The Call-by-Value Evaluation Strategy in the Lambda Calculus:

(\g -> (\x -> (g (x x)) \x -> (g (x x))) \f -> \term -> (((\g -> (\x -> (g (x x)) \x -> (g (x x))) \f -> \i -> \ps -> ((((\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> a) ps)) i) (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> a) ps))) ((f i) (\p -> (p \a -> \b -> b) ps)))) term) ((\x -> \y -> \p -> ((p x) y) ((\x -> \y -> \p -> ((p x) y) \arg -> ((\m -> \n -> ((\p -> \q -> ((p q) p) ((\m -> \n -> (\n -> ((n \x -> \a -> \b -> b) \a -> \b -> a) ((\m -> \n -> ((n \n -> \f -> \x -> (((n \g -> \h -> (h (g f))) \u -> x) \u -> u)) m) m) n)) m) n)) ((\m -> \n -> (\n -> ((n \x -> \a -> \b -> b) \a -> \b -> a) ((\m -> \n -> ((n \n -> \f -> \x -> (((n \g -> \h -> (h (g f))) \u -> x) \u -> u)) m) m) n)) n) m)) \f -> \x -> (f (f (f x)))) (\p -> (p \a -> \b -> a) arg))) term)) ((\x -> \y -> \p -> ((p x) y) ((\x -> \y -> \p -> ((p x) y) \arg -> ((\m -> \n -> ((\p -> \q -> ((p q) p) ((\m -> \n -> (\n -> ((n \x -> \a -> \b -> b) \a -> \b -> a) ((\m -> \n -> ((n \n -> \f -> \x -> (((n \g -> \h -> (h (g f))) \u -> x) \u -> u)) m) m) n)) m) n)) ((\m -> \n -> (\n -> ((n \x -> \a -> \b -> b) \a -> \b -> a) ((\m -> \n -> ((n \n -> \f -> \x -> (((n \g -> \h -> (h (g f))) \u -> x) \u -> u)) m) m) n)) n) m)) \f -> \x -> (f x)) (\p -> (p \a -> \b -> a) arg))) term)) ((\x -> \y -> \p -> ((p x) y) ((\x -> \y -> \p -> ((p x) y) \arg -> ((\m -> \n -> ((\p -> \q -> ((p q) p) ((\m -> \n -> (\n -> ((n \x -> \a -> \b -> b) \a -> \b -> a) ((\m -> \n -> ((n \n -> \f -> \x -> (((n \g -> \h -> (h (g f))) \u -> x) \u -> u)) m) m) n)) m) n)) ((\m -> \n -> (\n -> ((n \x -> \a -> \b -> b) \a -> \b -> a) ((\m -> \n -> ((n \n -> \f -> \x -> (((n \g -> \h -> (h (g f))) \u -> x) \u -> u)) m) m) n)) n) m)) \f -> \x -> (f (f x))) (\p -> (p \a -> \b -> a) arg))) ((\f -> \term -> (((\arg -> ((\m -> \n -> ((\p -> \q -> ((p q) p) ((\m -> \n -> (\n -> ((n \x -> \a -> \b -> b) \a -> \b -> a) ((\m -> \n -> ((n \n -> \f -> \x -> (((n \g -> \h -> (h (g f))) \u -> x) \u -> u)) m) m) n)) m) n)) ((\m -> \n -> (\n -> ((n \x -> \a -> \b -> b) \a -> \b -> a) ((\m -> \n -> ((n \n -> \f -> \x -> (((n \g -> \h -> (h (g f))) \u -> x) \u -> u)) m) m) n)) n) m)) \f -> \x -> (f x)) (\p -> (p \a -> \b -> a) arg)) (f (\app -> (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) app)) term))) (f ((((\g -> (\x -> (g (x x)) \x -> (g (x x))) \f -> \m -> \var -> \term -> (((\g -> (\x -> (g (x x)) \x -> (g (x x))) \f -> \i -> \ps -> ((((\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> a) ps)) i) ((\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> a) ps)) i)) ((f i) (\p -> (p \a -> \b -> b) ps)))) ((\x -> \y -> \p -> ((p x) y) term) ((\x -> \y -> \p -> ((p x) y) var) ((\x -> \y -> \p -> ((p x) y) m) ((\x -> \y -> \p -> ((p x) y) f) \x -> \a -> \b -> a))))) ((\x -> \y -> \p -> ((p x) y) ((\x -> \y -> \p -> ((p x) y) \terms -> ((\m -> \n -> ((\p -> \q -> ((p q) p) ((\m -> \n -> (\n -> ((n \x -> \a -> \b -> b) \a -> \b -> a) ((\m -> \n -> ((n \n -> \f -> \x -> (((n \g -> \h -> (h (g f))) \u -> x) \u -> u)) m) m) n)) m) n)) ((\m -> \n -> (\n -> ((n \x -> \a -> \b -> b) \a -> \b -> a) ((\m -> \n -> ((n \n -> \f -> \x -> (((n \g -> \h -> (h (g f))) \u -> x) \u -> u)) m) m) n)) n) m)) \f -> \x -> (f (f (f x)))) (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> a) terms)))) \list -> ((((\m -> \n -> ((\p -> \q -> ((p q) p) ((\m -> \n -> (\n -> ((n \x -> \a -> \b -> b) \a -> \b -> a) ((\m -> \n -> ((n \n -> \f -> \x -> (((n \g -> \h -> (h (g f))) \u -> x) \u -> u)) m) m) n)) m) n)) ((\m -> \n -> (\n -> ((n \x -> \a -> \b -> b) \a -> \b -> a) ((\m -> \n -> ((n \n -> \f -> \x -> (((n \g -> \h -> (h (g f))) \u -> x) \u -> u)) m) m) n)) n) m)) (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) list)))) (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> a) list))) (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> b) list)))) (\p -> (p \a -> \b -> a) list)))) ((\x -> \y -> \p -> ((p x) y) ((\x -> \y -> \p -> ((p x) y) \terms -> ((\m -> \n -> ((\p -> \q -> ((p q) p) ((\m -> \n -> (\n -> ((n \x -> \a -> \b -> b) \a -> \b -> a) ((\m -> \n -> ((n \n -> \f -> \x -> (((n \g -> \h -> (h (g f))) \u -> x) \u -> u)) m) m) n)) m) n)) ((\m -> \n -> (\n -> ((n \x -> \a -> \b -> b) \a -> \b -> a) ((\m -> \n -> ((n \n -> \f -> \x -> (((n \g -> \h -> (h (g f))) \u -> x) \u -> u)) m) m) n)) n) m)) \f -> \x -> (f (f x))) (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> a) terms)))) \list -> ((\x -> \y -> \p -> ((p x) y) \f -> \x -> (f (f x))) ((\x -> \y -> \p -> ((p x) y) ((((\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> b) list)))) (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> b) list)))) (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) list))) (\app -> (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) app)) (\p -> (p \a -> \b -> a) list)))) ((((\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> b) list)))) (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> b) list)))) (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) list))) (\app -> (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> b) app)) (\p -> (p \a -> \b -> a) list))))))) ((\x -> \y -> \p -> ((p x) y) ((\x -> \y -> \p -> ((p x) y) \terms -> ((\m -> \n -> ((\p -> \q -> ((p q) p) ((\m -> \n -> (\n -> ((n \x -> \a -> \b -> b) \a -> \b -> a) ((\m -> \n -> ((n \n -> \f -> \x -> (((n \g -> \h -> (h (g f))) \u -> x) \u -> u)) m) m) n)) m) n)) ((\m -> \n -> (\n -> ((n \x -> \a -> \b -> b) \a -> \b -> a) ((\m -> \n -> ((n \n -> \f -> \x -> (((n \g -> \h -> (h (g f))) \u -> x) \u -> u)) m) m) n)) n) m)) \f -> \x -> (f x)) (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> a) terms)))) \list -> ((((\m -> \n -> ((\p -> \q -> ((p q) p) ((\m -> \n -> (\n -> ((n \x -> \a -> \b -> b) \a -> \b -> a) ((\m -> \n -> ((n \n -> \f -> \x -> (((n \g -> \h -> (h (g f))) \u -> x) \u -> u)) m) m) n)) m) n)) ((\m -> \n -> (\n -> ((n \x -> \a -> \b -> b) \a -> \b -> a) ((\m -> \n -> ((n \n -> \f -> \x -> (((n \g -> \h -> (h (g f))) \u -> x) \u -> u)) m) m) n)) n) m)) (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) list)))) (\lam -> (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) lam)) (\p -> (p \a -> \b -> a) list))) (\p -> (p \a -> \b -> a) list)) ((\x -> \y -> \p -> ((p x) y) \f -> \x -> (f x)) ((\x -> \y -> \p -> ((p x) y) (\lam -> (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) lam)) (\p -> (p \a -> \b -> a) list))) ((((\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> b) list)))) (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> b) list)))) (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) list))) (\lam -> (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> b) lam)) (\p -> (p \a -> \b -> a) list)))))))) \x -> \a -> \b -> a))))) (f (\app -> (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> b) app)) term))) ((\x -> \y -> \p -> ((p x) y) \f -> \x -> (f (f (f x)))) (\lam -> (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) lam)) (f (\app -> (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) app)) term))))) (\lam -> (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> b) lam)) (f (\app -> (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) app)) term)))))) (f ((\x -> \y -> \p -> ((p x) y) \f -> \x -> (f (f x))) ((\x -> \y -> \p -> ((p x) y) (f (\app -> (\p -> (p \a -> \b -> a) (\p -> (p \a -> \b -> b) app)) term))) (f (\app -> (\p -> (p \a -> \b -> b) (\p -> (p \a -> \b -> b) app)) term)))))) f) term))) \x -> \a -> \b -> a)))))

Hassle ← Written in Haskell

A minimalistic, untyped, functional language which compiles to the SEC virtual machine.

Features

• Pattern Matching
• Currying
• Point-free function compostion
• Interpreted on a virtualized symbolic architecture (SEC)
• OHIi, an interactive Hassle interpreter

SEC Architecture ← Written in Haskell

A virtual machine based off the symbolic architecture of the SEC.