The Church

The Church

Paradigm(s)	functional
Designed by	User:Blashyrkh
Appeared in	2026
Computational class	Turing complete
Reference implementation	Github
Influenced by	Lazy K
File extension(s)	.holy

The Church is a functional untyped esolang which uses, misuses and abuses Church encoding for numbers, hence the name. The Church is based on the following set of combinators:

+ m n f x = n f (m f x)
* m n f = n (m f)
^ m n = n m
0 f x = x
1 f x = f x
2 f x = f (f x)
...
9 f x = f(9) x

As one can see, +, * and ^ act as addition, multiplication and exponentiation of Church numerals respectively, and 0 - 9 act as corresponding numeric constants. But the language is capable of much more than integer arithmetics: actually, the basis of combinators is complete (see below).

Essentially The Church is Lazy K with different basis of combinators and different syntax.

Syntax

The Church programs consist of combinator symbols (see above) and parentheses. Whitespace is ignored. Comments start from # and continue to the end of the line.

Expressions are written in infix syntax. Every operator is a binary function which receive its arguments through currying. Since the language is untyped, any expression may also play a role of binary operator.

All operators are left-associative, and follow this precedence (from lowest to highest): + * ^ 0 1 2 3 4 5 6 7 8 9. Parentheses change the order of operation, and take the highest precedence. Sub-expressions used as operators have lower priority than all combinator symbols. All (sub-)expressions must contain an odd number of terms; that is, every operator must have two corresponding operands.

A few examples to clarify the rules:

# Left-associativity:
1+2+3+4+5   # equivalent to (((1+2)+3)+4)+5

# Priority
3*2^5+7*4   # equivalent to (3*(2^5))+(7*4)

# Parentheses to change natural evaluation order
(2+3)*5     # NOT equivalent to 2+3*5

# Weird operators
123         # 2 is the operator on 1 and 3, which are its operands

# Weird operator priority
12345       # equivalent to 12(345)

# Sub-expression operator priority
1(123)3+5   # equivalent to 1(123)(3+5), NOT (1(123)3)+5

# Syntax errors
12          # expression doesn't have an odd number of terms; 2 doesn't have enough operands
((2+3)(     # unbalanced parentheses

The result of such convention is this: while Church numerals are easily human-readable and -writable (for example, 42 can be written as 6*7 or 2^5+2*5), everything else looks completely MAD!

I/O

EXACTLY as of Lazy K. 256 (used for end of output with exit code 0) can be written in The Church as 4^4 or 2^8 or 224 or 232. And like Lazy K, The Church allows K 256 to be used as EOF.

User:Cleverxia found this short expression for EOF: (***10)1224.

Completeness of the basis

This combinator basis is complete because it can express multiple other complete bases. Particularly:

B = *^*1*
C = ***1^
K = ^**10 = ***10
W = ^**1(^+^)

S = +1^*(***1^) = (*(+1^)*)**1^

The expression for S combinator was first found by User:PkmnQ, which was later confirmed to be optimal by brute-force search.

Translation to and from Lazy K

Any The Church program can be translated to Lazy K program and vice versa. The translation is by no means optimal; translating a program to Lazy K and back would produce textually different (and much longer) programs that behaves exactly as the original one (however, quines would cease to be quines for obvious reason).

Translation from Lazy K

It's assumed that the Lazy K program being translated from is written in the combinator calculus style.

1. For each sub-expression with an even number of operators, add I to the beginning, e.g. (SS(KK)K(SS)) -> (SS(IKK)K(ISS))
2. For each sub-expression of length 5 and more, group their first three terms in brackets: (SS(IKK)K(ISS)) -> ((SS(IKK))K(ISS)). Repeat the process until only length-3 sub-expressions left.
3. Exchange the left and middle terms in each sub-expression: (K(SS(KIK))(SIS))
4. Replace each combinator with its corresponding The Church expression according to the following table:

Lazy K to The Church

Source	Replacement
I	1
K	(^**10)
S	(+1^*(***1^))

Translation to Lazy K

1. Group each sub-expression such that none have more than one operator, e.g.: (1+2+3*5) -> (1+2+(3*5)) -> ((1+2)+(3*5))
2. Rewrite into prefix notation: (+(+12)(*35))
3. Replace each The Church combinator according to the following table:

The Church to Lazy K

Source	Replacement
0	(SK)
1	I
2	(S(S(KS)K)I)
3	(SS(SS(SK))(S(KS)K))
4	(SII(S(S(KS)K)I))
5	(S(SIS)I(S(S(KS)K))I)
6	(SSI(SSS)(S(KS)K)I)
7	(S(SI)S(SSK(S(S(KS)K)))I)
8	(S(S(S(KS)K))I(S(S(KS)K)I))
9	(S(SI)(SSKI)(S(S(KS)K)))
+	(S(K(S(S(KS)(S(K(S(KS)K))))))K)
*	(S(K(S(S(KS)K)))K)
^	(S(K(SI))K)

Bracket abstraction algorithm

For further explanation an ordinary (for combinatory calculus) prefix syntax will be used. To distinguish it from The Church syntax the square brackets are used instead of parentheses, e.g.:

(+1^*(***1^)) = [*[1+^][**[1*^]] = [*[+^][**[*^]]

Note: This is considered a different language to help aid explanation for this section, not a syntactic extension of The Church.

A bracket abstraction algorithm is an algorithm which can be applied to lambda calculus expression to translate it into combinatory calculus expression with the chosen basis of combinators. Here's the algorithm specific for The Church basis.

I rule

λ x . x = [1]

K rule

λ x . F = [K [F]] = [**[*0][F]]   # where F doesn't contain x

Special case of K rule:

λ x . 1 = [K 1] = [S K] = [0]

Eta-reduction

Target position for application of other rules:

λ x . F x = [F]                   # where F doesn't contain x

Front-swap rule

Moves bound variable from the leftmost place of expression one step towards the rightmost position:

[x A B C D] = [^ A x B C D]

Emerge rule

This rule extracts bound variable from sub-expressions:

[A B [C D x] E F ...] = [[A B] [[C D] x] E F ...] = [* [C D] [A B] x E F ...]

Mid-swap rule

Moves bound variable from arbitrary place within an expression one step towards the rightmost position:

[A B x C D] = [[A B x] C D] = [^ C [A B x] D] = [* [A B] [^ C] x D]

Deduplication rule

Reduces number of occurrences of bound variable by 1:

[A x [B x C]] = [+ B A x C]

Special cases:

[A x [B x]]   = [+ ^ A x B]
[A x x]       = [+ ^ A x 1]
[A x [x B]]   = [+ 1 A x B]
[x [x B]]     = [2 x B]

The algorithm

1. Find the innermost lambda. If no lambdas left then the algorithm is FINISHED.
2. Count a number of occurrences of the bound variable within the inner expression of the lambda.
3. If 0: apply the "K rule", then go to step 1.
4. If 1: go to step 6.
5. If more than 1: go to step 10.
6. If the bound variable is at the rightmost place of the inner expression of the lambda, apply either the I rule or the eta-reduction rule, then go to step 1.
7. If the bound variable is at the leftmost place of the inner expression of the lambda, apply the front-swap rule, then go to step 6.
8. If the bound variable is within the ()-subexpression of the inner expression of the lambda, apply the emerge rule, then go to step 6.
9. Apply the mid-swap rule, then go to step 6.
10. Find a ()-subexpression containing multiple occurrences of bound variable (it may be the inner expression of the lambda itself).
11. Use front-swap rule, mid-swap rule and emerge rule to move two occurrences of the bound variable to positions suitable for the deduplication rule. Apply the deduplication rule, then go to step 2.

Examples

Cat

1

Hello, world!

(4*3^3(4*3^3+3(2^5(4*3^3+3(4*3^3(3^3+6((***10)1224(^**1(21^**1(^**)**)(2*7)***10)9+1)4*5^2)4*3^3+6)4^2*7+7)6^2+8)4*3^3)4*5^2+1)1(9*8)

Looping counter

*10(*1*)((^(+2^)^)*******^2(*1^(*1(^**))2*5)*^1***1(^1(*1^(*1(^**))6*7))*+1^***^2(+11)(^(+2^)^)1)

Kolakoski sequence

*10(*1*)((^+^12+^11)*^1(^(+1^+^)(^(+2^)^)*^**1(^+^11)*(21**^1(*1(**^1(*1^))**1(21**^1(+1(^1^*^1(*10(*1*)2)*^2(*10(*1*)1)*^))***^1*))**1^)*^12))1(+1(6*8)*^****1^)

Truth-machine

 ^1(^**10)*^1^)*(^1((***10)1(6*8(^*(***1^))(^**10)1224)))*(^1(^(6*8)((***10)1((^(+2^)(*1(^1^)3(21+)))1((^*(***1^))1(7*7)))))

Quine

1(8(2(8(2(7(0(5(3(0(5(2(3(9(0(0(5(2(3(1(9(2(1(1(1(1(8(5(6(3(8(0(2(6(0(5(3(2(1(9(5(7(2(1(4(5(2(2(2(0(2(1(1(7(5(6(2(1(5(3(8(0(1(2(5(2(0(4(5(2(0(1(6(5(7(0(9(0(5(9(2(1(8(1(2(5(2(0(4(5(2(0(5(9(2(9(5(9(0(5(9(2(1(3(3(1(4(1(2(5(2(0(4(5(2(0(5(9(2(9(5(9(3(9(0(0(5(2(0(5(2(0(5(9(2(2(2(2(2(9(5(3(2(2(5(9(2(2(2(1(2(2(8(5(9(3(9(0(5(2(0(5(2(2(9(2(9(3(9(0(1(1(8(2(7(2(7(3(5(0(2(7(2(8(0(1(2(2(9(5(2(2(2(2(9(5(9(2(1(1(2(5(9(2(2(0(5(3(0(5(9(2(2(2(2(0(5(2(2(2(0(4(0(***1(****^1(+1(**^1*))*^1^****1^**)(4*3*(1+3*3*4))(^+^*^**1(*1(^+^14**)***^1**+1^*****^1(*1(*1((^+^1^*^1(*10(*1*)0)++)*^1(^1^*^1(*10(*1*)4)*^1(^(312)(*10(*1*)(4+1)*213))*(***10)*31^)*+1(2*(4+214))))*^)+*1((^+*1(+1(3*4*4))***^1***)**)***^2(^1(2*412+213)*^)***^1**+1^**)***^1****^1(^1*)***^1(+1^)***^1***)*^1(^1(^**1(**^1*)*+1^****1^)*^10**1((^+*1(+1(3*4*4))**)*^1(^1(2*4^2+2^3)**))*^*^)***^1(^1(^****1^))***^1(^1(*10(*1*)224))***^1(***10)**1^)0)1)2)2)2)9)5)2)2)2)1)2)2)1)2)2)2)9)6)0)9)5)0)6)2)8)5)6)3)6)5)7)1)2)9)1)2)2)2)9)5)2)2)3)5)9)2)2)1)2)2)2)9)5)2)2)2)2)9)5)0)9)5)2)1)2)2)2)9)5)0)3)5)9)1)2)2)2)9)5)2)2)2)1)2)9)5)0)9)5)0)9)2)2)5)0)2)2)9)5)2)1)2)3)5)9)2)2)2)2)5)9)1)2)9)5)4)2)2)5)0)0)9)3)2)5)0)3)5)0)7)2)8)2)8)1)1)2)2)1)2)9)5)0)9)5)0)6)2)8)9)6)3)6)9)7)1)2)2)1)1)2)9)2)9)1)2)2)2)9)5)0)9)5)0)9)2)2)2)2)5)9)1)1)2)2)2)9)5)0)9)5)0)2)5)4)0)2)5)2)1)6)6)8)1)1)2)2)2)9)5)0)2)2)2)5)4)1)2)2)5)9)1

Implementation

• Multi-language interpreter (supports Lazy K, Crazy J, BLC, BLC8, and The Church): https://github.com/rs-blashyrkh/lazy-k

See also

• Combinatory logic
• Church numeral
• Lazy K