Functional programming from scratch (2) —— Church Boolean encoding

[!quote] About λ expression...
See detailsλ expression

⚠ This article is exported from Obsidian, there may be format deviations (such as links, Callout, etc.)
Address of this article:/oberon-zjt0806/p/18710283

λ calculation and λ algebra

In the previous section, we used the λ symbol system to build an expression system. From here, we will officially start using this system for algebraic applications. Before performing calculations, we need to build a symbol system.Algebraic operation system。

[!note] Naming is just a naming after all
Although we have used a lot of things like(+ x 1)etc., but they are just names we define, so whateverxstill+and1,AllJust a markThat's it, although we have given these symbols some familiar meanings based on past experience, in the current context of λ calculating, these things are stillNo definitionPass.

Church encoding

In order to enable λ calculationSpecific applicationOn computers and programs, it means that the λ algebra system must be able to represent the following two things—

• Value(Logical values, integers...)
• Operation(Operators, functions, operations...)

That is to say, these things need to be in the λ calculationMap to λ expression(Use expressions to represent).

[!tip]
To put it bluntly, Church code isA sort ofCompare values ​​and operationsEncoded as λ expressionThe process.

• But be careful! Church encodingNot the only oneThere are other encoding methods, such asScott encodingwait.
• The characteristics of Church encoding areValueExpressed asstarting pointPerform encoding and build other encodings based on it.

Church-Boolean Logical Coding

[!abstract] Church-Boolean Coding Summary
For easy reference, all the encoding definitions in this section are listed here. The main text is a relatively long derivation process.

DEF T = λx.λ
DEF F = λx.λ
DEF AND = λP.λQ.(P Q P)
DEF OR = λP.λQ.(P P Q)
DEF NOT = λP.λQ.(P F T)

First we need to build it through Church encodingBoolean computing system. The reason why Boolean algebra is chosen first is that the structure of Boolean algebra is simple, the properties are clear, and it is easier to construct.

Boolean algebra(Boolean Algebra) contains very simple content-

• Boolean domain\(\mathbb B\)Only includedTwo elements\(\mathrm T\)and\(\mathrm F\)
• Supports three basic operations\(\wedge\) 、\(\vee\)、\(\neg\) 。
• The operation is closed to the domain and for\(\wedge\)and\(\vee\)All are there\(\mathbb B\)The upper and lower bounds exist respectively

Conditional selection function

Before introducing the authenticity and false values ​​in Church-Boolean, let's take a look at itConditional selection function, the so-called conditional selection function is a ternary function like the following -

in\(c\)is a conditional value, the conditional selection function is based on\(c\)The value is\(x\)and\(y\)Make a choice in. It can be found that in fact, this conditional selection function corresponds to theTriple operatorc ? x : y。

We represent this operation asIF-THEN-ELSEForm, can be expressed as-

IF c THEN x ELSE y

It can be found that it is divided into 3 sub-

• IF c:judgecconditions;
• THEN x:whenc == trueWhen satisfied, choosex；
• ELSE y: When the above conditions are not true, choosey；

At this point, we can put these three partsabstractforThree λ expressions。

DEF cond = λc.λx.λy.(c x y)

becauseTrue and false valueCarrying fromcTherefore we usecTo encode true and false values.

True and False | True | False

Based on the above idea, we can define the true value of the logic through Church encoding.Tand false valuesF. discusscThe situation, by definition,condThe function should satisfy—

cond T x y => λc.λx.λy.(c x y) T x y => λx.λy.(T x y) x y => T x y => x
COND F x y => λc.λx.λy.(c x y) T x y => λx.λy.(F x y) x y => F x y => y

observeTwo-step conversion, we found

• Want to useT x y => x, then(T x) yMust happenη Conversion。
  • That is to say(T x)middleThe constraints do not take effect, free expression can be constructed(T x) == λ
    • Take it off againxThe application of unblocking the constraint pair means that we need to introduce a new constraint variable
    • So we can getT == λa.λ。
• Want to useF x y => y, then(F x) yMust happenBeta Reduction。
  • And further,(F x) == identity == λ
    • Similarly, take off the right onexThe application of the constraint pair is untie the constraint pair and introduces additional constraint variablesλa
    • thenF == λa.λ

[!tip] Techniques for counter-reduction
We know for the application(f x)When the contract is made, thefReplace constrained variables in the parameterx,For example(λ x) => x
Then, in turn, for a known expressionxIf you want to introduce constraints, orxAs a parameter, a new non-conflicting constraint naming is required.x => (λ x)。
Using this property is known(f x)Can be expanded in case off == λa.(f a)

^9b9507

After α conversion,aRenamed tox，bRenamed toy, we can get itTandFDefinition

DEF T = λx.λ
DEF F = λx.λ

Under this definitionTandFMapdated as a λ function, so it can be used as a conditional selection function.

The above definition can be substituted into an expression(c x y)Prove this coded by [[λ expression # reduction digestion|reduction]]Correctness——

[!warning] Note
Don't forget when reducingRight-bound law of variable constraintsandThe left-bound law of function application

(T T F) => (λx.λ λx.λ λx.λ)
    β|=> (λx.λy.(λx.λ) λx.λ) 
    α|=> (λy.(λa.λ) λx.λ)
    η|=> (λa.λ)
    α|=> (λx.λ) => T

(F T F) => (λx.λ λx.λ λx.λ)
    η|=> (λ λx.λ)
    β|=> (λx.λ) => F // alternatively, ==> identity F => F

Logical Operations | AND | OR | NOT

Next, we need to be correctLogical operationsI will use Church encoding, here are three typesBasic logical operationsofTrue value table——

XOR, NAND and other things can be combined based on these three basic operations. So let’s just define the above three basic operations.

Before officially starting, let's first look at something--TandFAll are mapped asfunction, then it means they canmutualAs functions and parametersConstitute a constraint pairIf you use it, can the constraints beContractand after the concessionresultWhat is it? Here is the reduction result of the mutual application of two basic functions-

T T => (λx.λ) (λx.λ) β|=> λy.(λx.λ) α|=> λy.(λa.λ) => λ
T F => (λx.λ) (λx.λ) β|=> λy.(λx.λ) α|=> λy.(λa.λ) => λ
[.]  T P => λ
        T P Q => P
F T => (λx.λ) (λx.λ) η|=> λ => identity
F F => (λx.λ) (λx.λ) η|=> λ => identity
[.]  F P => λ => identity
        F P Q => Q

^6686a8

It should be noted that theTandFIn-housexandyand outer constraintsyNothing to do, but appearedNaming conflict(If you want to expand it needs to do it onceα conversion), so actually hereTyesFree expression. In the above reduction process, we can summarize the following properties-

• IfTUsed as a function(T P)(inP,Q in {T, F}), then it will passBeta ReductionWillxReplace withPThis gives a new functorλ,andQNot allowedyconstraints.
  • Make this resultλThen as a function and pass in parametersQConstraint pairs, then the next step will occurη Conversion, eliminateλyConstraints will only be left in the endP（T P Q => λ Q => Q）
• IfFAs a function, then sinceFofλxandNo constraints are made, so do it firstη Conversion, eliminateλxConstraints will always be left behindλ, by chance, this happened to beIdentity functionidentity
  • Then it will be very clear next, if you pass in parameters againQ,becauseidentitynature, or directly throughBeta ReductionReplace, only the following parameter will be leftP（F P Q => identity Q => λ Q => Q）

![Church T ]]

The above work helps us to use Church encodingDefine logical operations。

Collect | and | AND

First, let’s take a look at the combined operation. The requirement for combined is that only when both inputs areTOnly then can it be reduced toT, all other situations areF——

AND T Q => Q
    AND T => (F P)
AND F Q => F
    AND F => (T P)

Observe the above form, forAND P Q, we can make the following summary

• whenP==Thour,AND P Q => AND T Q => Q
  • This situation corresponds to [[#^6686a8|above]](F P),thenAND T Q => F P Q
• whenP==Fhour,AND P Q => AND F Q => F
  • This situation corresponds to [[#^6686a8|above]](T P),thenAND F Q => T P Q

[!question] I'm in trouble
The conclusion we have now summarized isAND P == (NOT P) P, however, the problem is that we stillNo definitionNOT, what should I do?

[!tip] OK
ANDsatisfyExchange law, that is, there should beAND P Q == AND Q P

Through the law of exchangeAND P QChange toAND Q P, does not affect the previous conclusion, except for the discussion object at this timeAND PBecomeAND Q。

AND Q P[P:=T] => Q
    AND Q => (T Q)
AND Q P[P:=F] => AND Q F => F
    AND Q => (F Q)
AND Q => (P Q)

Finally we can come up withANDChurch code-

DEF AND = λP.λQ.(P Q P)

Disjunction | or | OR

With the combinationsimilar, also hasExchange law, and we canFollow the example just nowThe process is completedORFirst, the definition of

OR T Q => T
    OR T => (T P)
OR F Q => Q
    OR F => (F P)

This time, there is no need to exchange rules, you can get it by just replacing it.ORDefinition-

DEF OR = λP.λQ.(P P Q)

Reversal | Non | NOT

NOTMore special becauseNOTIt's oneOne dollarOperations need to be discussed separately.

NOT T == NOT λx.λ => F == λx.λ
NOT F == NOT λx.λ => T == λx.λ

Simply put, the input parameters are to select one of them, thenNOTThe output is always selected. Considering the true valueTandFAll are passedconddefined, then, ifDirect reversalcondofdefinitionCan you get the opposite output?

cond == λc.λx.λy.(c x y)
ncond == λc.λx.λy.(c y x)

So we gotA sort ofNOTThe definition form

DEF NOT1 = λP.λx.λy.(P y x)

This form looks quite low-level. Can we use the existing onesLogical valueTo define it?

Check againcond P ——

cond P => λP.λx.λy.(P x y) P => λx.λy.(P x y)

If consideringxReplace withF，yReplace withT, the same effect can be achieved, so we further provide parameters-

cond P F T => λx.λy.(P x y) F T => P F T

So we gotAnotherNOTDefinition-

DEF NOT2 = λP.(P F T)

It can be proved by the reduction,NOT1 <=> NOT2

At this point, two logical values ​​and three basic logical operations areDefinition is complete, Church-Boolean encoding is completed, and you can use the λ expression for logical calculation.

[!question] Thinking
Try to define more logical operations in a similar way, such as ExorXOR, and nonNANDwait……