Church Encoding

A functional programming exercise in PHP demonstrating how data and logic can be represented purely using functions.

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

Church encoding is not intended as a practical implementation of primitive data types. Its main purpose is to show that primitive data types are not necessary to represent any computation. More information on Wikipedia.

History

This library was created for personal educational purposes and made public. It was inspired by the work of Marcelo Camargo.

Although available via Composer and Packagist, this library is primarily useful for learning and experimentation rather than production use.

Installation

composer require loophp/church-encoding

Quick Example

use Loophp\ChurchEncoding\Church;

// Church numerals
$zero = Church::zero();
$one = Church::succ($zero);
$two = Church::succ($one);

// Church booleans
$true = Church::true();
$false = Church::false();

echo $two->toInt(); // 2

Documentation

Church numerals

Imagine a programming language that doesn’t support numbers or booleans, only lambdas. Could we still represent counting, addition, and multiplication? Yes: that’s the idea behind Church numerals.

A Church numeral is a function with two parameters: λf . λx . something

• The first parameter f is the successor function.
• The second parameter x represents zero.

Examples:

• C0 = λf . λx . x
• C1 = λf . λx . f x
• C2 = λf . λx . f (f x)

Each numeral applies the successor function f as many times as its numeric value. We can count, add, or multiply using these forms — though to “see” the result, we must count the applications of f manually.

Church booleans

Booleans can also be represented using functions:

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

These can be used to define logic operators:

• 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 by Robert “Corky” Cartwright
• Gabriel Lebec: Part 1 and Part 2
• Package loophp/combinator
• Lambda calculus on Wikipedia
• Church encoding on Wikipedia
• Programming with Less Than Nothing

Code Quality, Tests and Benchmarks

Every change triggers automated tests via GitHub Actions.

• Tests are written with PHPSpec (composer phpspec)
• Static analysis via PHPStan and Psalm
• Mutation testing with Infection (composer infection)
• Pre-commit checks with GrumPHP (composer grumphp)

Contributing

Contributions are welcome! Send a pull request on GitHub.

If you prefer to support my open-source work financially, you can sponsor me on GitHub or PayPal.

Project Status

This project is feature-complete and stable. It is maintained for educational purposes and may receive occasional compatibility updates.

Changelog

See CHANGELOG.md for the commit-based changelog. For detailed release notes, visit the release page.