semvec/pypi-packages huggingface dataset:
churchrepl 1.0.2
A simple REPL for lambda calculus
License: BSD

CHURCH-REPL
===========

A simple REPL for lambda calculus

.. image:: https://travis-ci.org/CodeGrimoire/ChurchREPL.svg?branch=master
    :target: https://travis-ci.org/CodeGrimoire/ChurchREPL

Use:
----
when calling churchrepl and new REPL will be opened.

.. code-block::

    churchrepl [-f --file file [file ...]] [-v --verbose]

Flags:

(optional) Read definitions and expressions from a file before loading the normal REPL.

.. code-block::
    
    -f|--file file [file ...]


(optional) print debugging and verbose output.

.. code-block::
    
    -v|--verbose


Church repl file structure:
---------------------------

The EBNF grammar is as follows*:

::

   (* church-lambda EBNF *)
                     (* --- meta --- *)
    program = {line};
    line = (define | function);
    define = "@" alias ":" function;

                     (* --- lambdas --- *)
    function = lambda | application;
    lambda = "λ" variable "." expr;
    application = '(' expr  expr ')';
    expr = (lambda | application | variable | alias );

                     (* --- primitives --- *)
    variable = /[a-z]/;
    alias = /[_A-Z][_A-Z0-9]*/;

A simple example program:

::

    @ID: λx.x
    @APPLY: λf.λx.(f x)
    @TRUE: λx.λy.x
    @FALSE: λx.λy.y
    @ZERO: λf.λx.x
    @SUCC: λn.λf.λx.(f ((n f) x))
    @ONE: (SUCC ZERO)
    @TWO: (SUCC ONE)
    @THREE: (SUCC TWO)
    @FOUR: (SUCC THREE)
    (SUCC ZERO)
    (SUCC ONE)
    (SUCC TWO)
    (SUCC THREE)
    (SUCC FOUR)

Note: The λ (lambda, unicode u03bb) is equivalent to a backslash as far as this program is concerned.
When using the repl it may be easier to use a backslash.