.. _ChurchNumerals:

.. raw:: html

   <script>ODSA.SETTINGS.DISP_MOD_COMP = true;ODSA.SETTINGS.MODULE_NAME = "ChurchNumerals";ODSA.SETTINGS.MODULE_LONG_NAME = "Church Numerals and Booleans";ODSA.SETTINGS.MODULE_CHAPTER = "Lambda Calculus"; ODSA.SETTINGS.BUILD_DATE = "2018-03-22 16:52:21"; ODSA.SETTINGS.BUILD_CMAP = false;JSAV_OPTIONS['lang']='en';JSAV_EXERCISE_OPTIONS['code']='java_generic';</script>


.. |--| unicode:: U+2013   .. en dash
.. |---| unicode:: U+2014  .. em dash, trimming surrounding whitespace
   :trim:


.. This file is part of the OpenDSA eTextbook project. See
.. http://algoviz.org/OpenDSA for more details.
.. Copyright (c) 2012-13 by the OpenDSA Project Contributors, and
.. distributed under an MIT open source license.

.. avmetadata:: 
   :author: David Furcy and Tom Naps

.. odsalink::  AV/PL/AV/church_string.css

Church Numerals and Booleans
============================

Church Booleans
---------------

To turn the  :math:`\lambda` calculus into a "real" programming language, we
need to be able to manipulate:

-  boolean constants (true, false)
-  logical operators (and, or, not)
-  conditionals (if)
-  integers (0, 1, 2, 3, etc.)
-  arithmetic operators (:math:`+`, :math:`-`, etc.)
-  mathematical functions (factorial, etc.)

Alonzo Church, the creator of the :math:`lambda` calculus, realized
this and consequently set about to make a series of encodings of
lambda expressions designed to satisfy the properties we expect from
the items in the preceding list.  Let's first examine some of the encodings for the
*church boolean* constants and operations.

-  TRUE = :math:`\lambda x.  \lambda y.x`
-  FALSE = :math:`\lambda x.  \lambda y.y`
-  AND = :math:`\lambda p. \lambda q.((p \; q) \; FALSE)`

The following slideshow indicates how TRUE AND FALSE is :math:`\beta` reduced.
   
.. inlineav:: church_bool ss
   :points: 0.0
   :required: False
   :threshold: 1.0
   :long_name: Church boolean slideshow
   :output: show

As one would expect for boolean operations, TRUE AND FALSE reduces to FALSE. 
   

Encoding If-Then-Else
---------------------

This problem is about a possible representation for the ternary IF/THEN/ELSE
operator.

.. avembed:: Exercises/PL/ChurchIfThen.html ka
   :module: ChurchNumerals
   :points: 1.0
   :required: True
   :threshold: 1
   :exer_opts: JXOP-debug=true&amp;JOP-lang=en&amp;JXOP-code=java_generic
   :long_name: If Then Else in Church Encoding

Encoding OR
-----------

This problem is about a possible representation for the binary OR
operator.

.. avembed:: Exercises/PL/ChurchOR.html ka
   :module: ChurchNumerals
   :points: 1.0
   :required: True
   :threshold: 1
   :exer_opts: JXOP-debug=true&amp;JOP-lang=en&amp;JXOP-code=java_generic
   :long_name: Church Encoding for OR


Church Numerals
---------------

To encode the non-negative integers, Church used the following encoding:

-  ZERO = :math:`\lambda f. \lambda\ x.x`

-  A successor function SUCC = :math:`\lambda n. \lambda f. \lambda x.(f \; ((n \; f) \; x))`

-  ONE = (SUCC ZERO) = :math:`\lambda f. \lambda\ x.(f \; x)`

-  TWO = (SUCC ONE) = :math:`\lambda f. \lambda\ x.(f \; (f \; x))`

-  THREE = (SUCC TWO) = :math:`\lambda f. \lambda\ x.(f \; (f \; (f \; x)))`

-  FOUR = (SUCC THREE) = ???

-  FIVE = (SUCC FOUR) = ???

-  SIX = (SUCC FIVE) = ???

-  SEVEN = (SUCC SIX) = ???

-  EIGHT = (SUCC SEVEN) = ???

-  NINE = (SUCC EIGHT) = ???

-  TEN = (SUCC NINE) = ???

To help you see how the successor function works, watch the following slideshow of how the successor of THREE is reduced to FOUR.
   
.. inlineav:: church_numeral ss
   :points: 0.0
   :required: False
   :threshold: 1.0
   :long_name: Church numeral slideshow
   :output: show

Addition and multiplication can be encoded as:
	    
-  PLUS = :math:`\lambda m. \lambda n. \lambda f. \lambda x.((n \;f) \; ((m \; f) \; x))`

-  MULT = :math:`\lambda m. \lambda n. \lambda f.(m \; (n \; f))`

To see how the multiplication function works, watch the following slideshow of how (MULT TWO THREE) reduced to SIX.
   
.. inlineav:: church_mult ss
   :points: 0.0
   :required: False
   :threshold: 1.0
   :long_name: Church multiplication slideshow
   :output: show

An encoding for a predecessor operation:

PRED = :math:`\lambda n. \lambda f. \lambda x.(((n \; \lambda g. \lambda h.(h \; (g \; f))) \lambda u.x) \; \lambda u.u)`

And an operation to test for zero in an **if-then-else**    

ISZERO = :math:`\lambda n.((n \; \lambda x.FALSE) \; TRUE)`

	    

Church numerals with addition and multiplication
------------------------------------------------

This problem will help you recognize and use the Church numerals as
well as the representation of the corresponding addition and
multiplication operators. To get credit for this randomized problem,
you must solve it correctly three times in a row.

.. avembed:: Exercises/PL/ChurchNumerals.html ka
   :module: ChurchNumerals
   :points: 1.0
   :required: True
   :threshold: 3
   :exer_opts: JXOP-debug=true&amp;JOP-lang=en&amp;JXOP-code=java_generic
   :long_name: Church Numerals



.. odsascript:: AV/PL/AV/church_bool.js
.. odsascript:: AV/PL/AV/church_numeral.js
.. odsascript:: AV/PL/AV/church_mult.js