Language Documentation

Github Other systems

Untyped-Lambda calculus implementation

Editor

During typing, following shortcuts are working.

CTRL+S

Run code.

CTRL+I

Show trace tab.

CTRL+O

Show output tab.

CTRL+H

Show help tab.

Application rules

Application is left-associative.

f x g x is equal to ((f x) g) x

Applicaiton of variable-terms separated by whitespace.

f x: apply x to f

ff x: apply x to ff

Simple form

Syntax form

(\x.(\y.(x))) β= \x.\y.x

(((\x.(\y.(x))) a) b) β= (\x.\y.x) a b

\f.\g.\x.((f x) (g x)) β= \f.\g.\x.f x (g x)

Comments

-- ...

Comment to the end of the line.

Examples

I-combinator: \x.x

(\x.x) a

constant: \y.x

(\y.x) a

Nested applications

(\f.λx.f (f x)) (\y.y z) a

Alpha-convertion

(\x.\y.x y) y a

SKK-combinator

(\f.\g.\x.f x (g x)) (\x.\y.x) (\x.\y.x) a