Calchylus 3 - Lambda calculus with Hy
Intro
calchylus3 is a computer installable Hy_ module that is used to evaluate,
and furthermore through this documentation, shine light to the basics of Lambda
calculus (also written as λ-calculus).
`Lambda calculus`_ is a formal system in mathematical logic for expressing
computation that is based on function abstraction and application using
variable binding and substitution.
The target audience is those who:
a) are interested in the theory and the history of the programming languages b) may have or are interested to gain some experience in Python and/or Lisp c) who wants to narrow the gap between mathematical notation and programming languages, especially by the means of logic
Andrew Bayer_ writes in his blog post about formal proofs and deduction:
*Traditional logic, and to some extent also type theory, hides computation
behind equality.*
Lambda calculus, on the other hand, reveals how the computation in logic is
done by manipulation of the Lambda terms. Manipulation rules are simple and
were originally made with a paper and a pen, but now we rather use computers for
the task. Lambda calculus also addresses the problem, what can be proved and
solved and what cannot be computed in a finite time. Formally these are called
the decidability_ and the halting_ problems.
Beside evaluating Lambda expressions, calchylus3 module can serve as a
starting point for a mini programming language. Via custom macros_
representing well known Lambda forms, calchylus3 provides all necessary
elements for boolean, integers, and list data types as well as
conditionals, loops, variable setters, imperative do structure, logical
connectives, and arithmetic operators. You can build upon that, for example
real numbers_ , even negative complex numbers if that makes any sense. Your
imagination is really the only limit.
Finally, when investigating the open source calchylus3 implementation that is
hosted on GitHub_ , one can expect to get a good understanding of the higher
order functions and the combinatory logic_ , not the least of the fixed point
combinator or shortly, Ï’ combinator.
Quick start
For people willing to get hands quickly on coding:
Install
.. code-block:: bash
$ pip install calchylus3
Open Hy
.. code-block:: bash
$ hy
Import lambda library
.. code-block:: hylang
(require [calchylus3.lambdas [*]])
Initialize lambda macros
.. code-block:: hylang
(with-macros L)
Lambda dance
.. code-block:: hylang
(print* ((L x y [x [x y]]) 'a 'b)) ; output: (a (a b))
.. code-block:: hylang
(print* (FIBONACCI SEVEN 'x 'y)) ; output: (x (x (x (x (x (x (x (x (x (x (x (x (x y)))))))))))))
Documentation
For full documentation, see: calchylus3.readthedocs.io_
.. |Output:| replace:: [output]
.. _halting problem: http://www.huffingtonpost.com/entry/how-to-describing-alan-turings-halting-problem-to_us_58d1ae08e4b062043ad4add7 .. _combinatory logic: https://en.wikipedia.org/wiki/Combinatory_logic .. _GitHub: https://github.com/markomanninen/calchylus3 .. _real numbers: https://cs.stackexchange.com/questions/2272/representing-negative-and-complex-numbers-using-lambda-calculus?noredirect=1&lq=1 .. _my favorite programming language: http://www.python.org .. _custom macros: http://calchylus.readthedocs.io/en/latest/macros.html .. _decidability: https://plato.stanford.edu/entries/computability/#UnsHalPro .. _Andrew Bayer: http://math.andrej.com/2016/08/30/formal-proofs-are-not-just-deduction-steps/ .. _Lambda calculus: https://en.wikipedia.org/wiki/Lambda_calculus .. _Hy: http://docs.hylang.org .. _calchylus3.readthedocs.io: http://calchylus3.readthedocs.io/
