Implementation of a Combinatory Logic (SKI calculus) reducer in F#, running interactively in the console. It parses user input to combinatory logic terms and performs a series of contractions to find the weak normal form, printing the response on the screen. If a term has no weak normal form, it displays an error message. If the input is incorrect or invalid, an error message is also displayed.

Install .NET. Then, just navigate to the project directory:

    cd ~/../yourstuff/Reducer/Reducer

To build and run:

    dotnet build -c Release
    dotnet ./bin/Release/net5.0/Reducer.dll

To build and run as a standalone .exe:

    dotnet publish -c Release -o [YOUR_DIRECTORY]

To test:

    cd ~/../yourstuff/Reducer/ReducerTests
    dotnet test

I could not make it able to detect if a term has no weak normal form using the quasi-leftmost reduction theorem. I also think it's not possible to use the theorem in a program, because there's no way to generalize an algorithm to pick the correct non-leftmost reductions for every irreducible term.

Lambda-Calculus and Combinators - An Introduction