You can write lambda expressions in the input box.
Variable names are lowercase letters and may be followed by a number 0-9 (a, b, a0, w8)
Functions can be written with \ or / instead of λ and there is support for multiple arguments: /ab.a is the same as /a./b.a
Applications must be written between (). Also, there can be more than two arguments: (a b a b c) is the same as ((((a b) a) b) c). This is the left to right priority
Another type of applications is written between []. This is the right to left priority: [a b a b c] is the same as (a (b (a (b c))))
If enabled, numbers(in decimal base) will be transformed to their Church encoding counterpart.
Once you have written an expression and it has been parsed, you can β-reduce it
You can β-reduce it a single step or as many as needed to achive the β-normal form
Be careful because the last option can not be stopped, so if an expression does not have a β-normal form, it will fun forever
Reduced forms will not retain the names of the variables and will use the earliest possible, maybe even longer than one charachter. This is only a way of representing it
Reduced forms will show unbound variables as U + a number
You can define useful functions in the define menu. Then, you can use them by preceding the # symbol to the name (for example #add)
The definitions should be entirely self-contained and independent, because thats how they will be parsed
There are some pre-defined functions, used with boolean logic and basic arithmetic
This interpreter has an option to generate Tromp diagrams. These diagrams make it easy to see how the terms correlate graphically
The generated images are bitmaps and can be downloaded
Internally, this interpreter works with De Bruijn indexing. Thats the reason why there is no name retention