Skip to content

Here is a simple interpreter for beta-reduction of terms, which has been implemented using de Bruijn (de Braun) notation.

Notifications You must be signed in to change notification settings

OganyanRV/Beta-reduction

Repository files navigation

Lambda-Calculus. Beta-reduction of lambda terms with de Braun indices

This repository is outdated. The actual project is here. The problem with this version is that I do not use an abstract syntax tree to find redexes, I look for them in a string, which works, but it is ideologically wrong.

Course work of Oganyan Robert. Third year of study, 6th term.

Here is a simple interpreter for beta-reduction of terms. Beta reduction of lambda terms has been implemented using de Bruijn (de Braun) notation and related: alpha conversions, naming contexts, shifts and substitutions.

Implemented with C++14, JetBrains Clion.

Work demonstration

Gif

work_demo

Screenies

Start screen.

img

Rule's list.

img

Starting own-written tests.

img

Lets reduce this term: img .

img

That is correct.

Now lets try this one: img The result should be img.

img

Correct. Now lets calculate (0 + 2 * 1) = 2

img

We are having img. Reduction has been done correct.

Quit the program.

img

About

Here is a simple interpreter for beta-reduction of terms, which has been implemented using de Bruijn (de Braun) notation.

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published