README

Church Encoding

In mathematics, Church encoding is a means of representing data and operators in the Lambda calculus. The Church numerals are a representation of the natural numbers using Lambda notation. The method is named for Alonzo Church, who first encoded data in the Lambda calculus this way.

The Church encoding is not intended as a practical implementation of primitive data types. Its use is to show that other primitive data types are not required to represent any calculation. The completeness is representational...more on Wikipedia.

History

This library has been done for personal educational purpose and made public, it has been inspired by the work of Marcelo Camargo. The code is available through Composer(via Packagist) just in case, but I doubt this will be useful for anyone beside learning purposes.

Usage

composer require loophp/church-encoding

Documentation

Church numerals

Assume we have a programming language that doesn’t support numbers or booleans: a Lambda is the only value it provides. It is an interesting question whether we can nonetheless create some system that allows us to count, add, multiply, and do all the other things we do with numbers.

Church numerals use Lambdas to create a representation of numbers.

The idea is closely related to the functional representation of natural numbers, i.e. to have a natural number representing zero and a function succ that returns the successor of the natural number it was given. The choice of zero and succ is arbitrary, all that matters is that there is a zero and that there is a function that can provide the successor. Church numerals are an extension of this.

All Church numerals are functions with two parameters: λf . λx . something

The first parameter f is the successor function that should be used. The second parameter x is the value that represents zero.

Therefore, the Church numeral for zero is: C0=λf . λx . x

Whenever it is applied, it returns the value representing zero. The Church numeral for one applies the successor function to the value representing zero exactly once: C1=λf . λx . f x.

The Church numerals that follow just have additional applications of the successor function

It is important to note that in this minimal Lambda calculus, we can’t really do very much with these Church numerals. We can count and add and multiply, but to understandthe result, we have to count the applications of the successor function.

Church booleans

We can ask the same question we asked about numbers about booleans. Can we represent them using just functions? Yes we can, and in a way very similar to Church numerals. A Church boolean is a function with two parameters, the first represents what the function should return if it is true, the second what the function should return if it is false:

true = λx . λy . x
false = λx . λy . y

Just like with Church numerals, we can also perform arithmetic with Church booleans.

It is easy to define functions for and, or, and not

and = λM . λN . M (N true false) false
or = λM . λN . M true (N true false)
not = λM . M false true

References

Types And Programming Languages (TAPL)
Structure and Interpretation of Computer Programs (SICP)
Lectures of Robert ”Corky” Cartwright
Gabriel Lebec: Part 1 and Part 2
Package loophp/combinator
Lambda calculus on Wikipedia
Church encoding on Wikipedia

Code quality, tests and benchmarks

Every time changes are introduced into the library, Github run the tests.

The library has tests written with PHPSpec. Feel free to check them out in the spec directory. Run composer phpspec to trigger the tests.

Before each commit some inspections are executed with GrumPHP, run composer grumphp to check manually.

The quality of the tests is tested with Infection a PHP Mutation testing framework, run composer infection to try it.

Static analysers are also controlling the code. PHPStan and PSalm are enabled to their maximum level.

Contributing

Feel free to contribute by sending Github pull requests. I'm quite reactive :-)

If you can't contribute to the code, you can also sponsor me on Github or Paypal.

Changelog

See CHANGELOG.md for a changelog based on git commits.

For more detailed changelogs, please check the release changelogs.

loophp / church-encoding

Maintainers

Details