combinatory logic
Combinatory Logic II
9/18/19
As in the lambda calculus, there are the notions of redex, reduction path, normal form...
Combinatory logic is going to do away with the abstractions of lambda calculus. Doing this is known as bracket abstraction and the bracket abstraction algorithm removes all abstractions from lambda expressions and replaces them with a standard combinator expression.
Lambda Calculus and Combinatory Logic
2013
The lambda calculus is the calculus or logic of (anonymous) functions. Examples of very simple functions in mathematics include double[x] which takes 1 to 2, 2 to 4 etc and square[x] which takes 1 to 1, 2 to 4 etc. And there are functions in daily life, for example motherOf[x] takes one person to another. The example functions have explicit names, eg 'double'. Lambda calculus deals with functions, but typically without giving the functions names. The functions are anonymous functions.
Roll your own [Combinatory Logic]
2018
You can try your own exercises here. Type in, or edit, in the lower panel then select and press 'Start from selection'. To show the starting formula for a reduction and the target formula, use the double headed arrow and put the start to the left and the target to the right.