loophp / church-encoding
Church encoding in PHP
Fund package maintenance!
drupol
www.paypal.me/drupol
Requires
- php: >= 7.4
- loophp/combinator: ^2.0
Requires (Dev)
This package is auto-updated.
Last update: 2024-10-09 14:19:39 UTC
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.