User:Blashyrkh/The Church

This is still a work in progress. It may be changed in the future.

This is a draft page. It's messy, it's incomplete, it's a subject of change. It is (and it will be) 100% AI-free: the concept, the design, the (future) reference implementation and the page (including formatting and wording) are/will be made by mad human mind(s) only. If you're reading this text and desire to improve it with AI then I can't stop you due to the nature of the CC0 license. But I ask you not to. Just find another victim.

The language uses, misuses and abuses Church encoding, hence the name. The name is not final, it may change if I find something more appropriate. The Church is a functional untyped language based on the following combinators:

+ = λmnfx . nf(mfx)
* = λmnf . n(mf)
^ = λmn . nm
0 = λfx . x
1 = λfx . fx
2 = λfx . f(fx)
...
9 = λfx . f(9)x

Completeness of the basis

This combinator basis is complete because BCKW combinators can be expressed in this basis:

B = *^(**)
C = **(*^)
K = *^(*0) = **(*0)
W = *^(*(+^^))

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

Note: first version of S was suggested by User:PkmnQ, and it happened to be optimal (size 7).

And the other way:

+ = S(K(S(S(KS)(S(K(S(KS)K))))))K
* = S(K(S(S(KS)K)))K
^ = S(K(SI))K
0 = SK
1 = I
2 = S(S(KS)K)I
3 = SS(SS(KI))(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))

Syntax

The Church program consists of combinators characters (digits 0-9, +, * and ^) and brackets ( and ). White space is ignored, everything starting from # to the end of the line is a comment.

Brackets has an ordinary meaning - they control evaluation order. Sub-expression within a pair of brackets - as well as the top-level program expression - MUST contain ODD number of operands (combinators or sub-expressions), otherwise the program is syntactically invalid.

If there are exactly 3 operands within a pair of brackets, they are interpreted in the following order:

(ARG1 OPERATOR ARG2)   

The expression above means "apply OPERATOR function to ARG1 and then (the returned function) to ARG2" (currying). E.g.: The Church expression (6*7) in normal combinator calculus would be written as * 6 7. There's no limitations what can/can't be an "operator" and what can/can't be an "argument": ^*(*10) is syntactically valid The Church code (it's actually K combinator written according to The Church syntactic rules).

If more than 3 operands (5, 7, 9...) are within a pair of brackets, then operands at even (1-based) positions (2, 4...) are considered operators and operands at odd positions - their arguments. The evaluation order is determined by operator precedence (from lowest to highest: +*^0123456789) and left-associativeness. So, (2+6^2+4) is equivalent to ((2+(6^2))+4), and the example above (K combinator ^*(*10)) can be written without brackets: ^**10 (because 1's precedence is higher than *'s one).

The result of such syntax convention is this: while Church numerals can be easily read and written by mere humans (Church numeral 42 is written as 6*7 or 2^5+2*5), everything else looks completely MAD!

IO

EXACTLY as of Lazy K. EOF constant in The Church can be written as 4^4 or 2^8. And like Lazy K, The Church allows (K 256) ((***10)1(2^8) in The Church infix notation) be used as EOF.

Translation to and from Lazy K

The Church program can be translated into Lazy K program and vice versa (but probably in most cases the result of going there and back again would be much larger than the origin). This fact also proves Turing Completeness of The Church (Lazy K is proven to be Turing Complete).

Translation from Lazy K

Hereafter it's assumed that Lazy K's combinator calculus style is used for original program. The translation procedure is defined as follows:

1. Ensure that each sub-expression (top-level or enclosed into pair of matching brackets) contains ODD number of arguments. If it's not, insert I at the beginning. E.g. (SS(KK)K(SS)) -> (SS(IKK)K(ISS))
2. For each sub-expression of length 5 and more: enclose first three terms of the sub-expression into a pair of brackets: (SS(IKK)K(ISS)) -> ( ( SS(IKK) ) K(ISS)). Repeat the process until only length-3 sub-expressions left.
3. Exchange the leftmost and the middle terms of each sub-expression: (K(SS(KIK))(SIS))
4. Replace each term with an expression according to the table below

Lazy K to The Church

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

Translation to Lazy K

1. For each sub-expression of length 5 and more: inspect all even-indexed (1-based) terms, find the one with the highest precedence (if there are several such terms then choose the leftmost one) and enclose it and its neighboring terms into a pair of brackets. Repeat until only 3-term sub-expressions left. E.g.: (1+2+3*5) -> (1+2+(3*5)) -> ((1+2)+(3*5))
2. Exchange the leftmost and the middle terms of each sub-expression: ((1+2)+(3*5)) -> (+(+12)(*35))
3. Replace each term with an expression according to the table below

The Church to Lazy K

Source	Replacement
0	(SK)
1	I
2	(S(S(KS)K)I)
3	(SS(SS(KI))(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)

Other combinators in The Church basis

It's just the raw output of my bruteforcer. The Church expressions are shown in CC prefix notation, not in The Church infix notation:

Found solution for W' (3): +^^
Alternative solution for W' (3): *^2
Found solution for Q2 (3): *^*
Found solution for K (4): *^(*0)
Found solution for B (4): *^(**)
Found solution for C (4): **(*^)
Found solution for H (4): *+(^^)
Found solution for Q3 (4): **(^^)
Found solution for M2 (4): +(+^)^
Found solution for W (6): +(+^)(*0^)
Found solution for R (5): 2(*^)(**)
Found solution for Q4 (6): 2(*^)(2(**))
Found solution for M (6): 2(^^)(+(+^))
Improved solution for M (6 > 5): 3(^^)(2+)

Examples

Cat

1

Hello, world!

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

QUINE

Soon...

TODO

1. ☑️ Add The Church syntax mode to my Lazy K interpreter
2. 🔲 Few improvements to my Lazy K + The Church interpreter:
   1. 🔲 Verbosity about syntax errors (currently implemented only for The Church mode)
   2. ☑️ CC Lazy K syntax support (currently only unlambda-style is supported)
   3. ☑️ Crazy J too (3 syntax modes)
3. 🔲 Publish the interpreter at github (at last)
4. 🔲 The article:
   1. Preamble
      1. Language class
      2. Unusual infix syntax
      3. Name
   2. Combinator basis
      1. Define combinators
      2. Prove basis completeness
      3. Other well-known combinators in The Church basis (both CC and infix syntax)
   3. Syntax
      1. Examples of infix syntax
      2. OPs priorities
   4. IO
   5. Translation to and from Lazy K
   6. Interpreter
      1. Where to get, how to build, how to use
      2. Multi-language interpreter, supports BLC, BLC8, Lazy K, The Church and (will be) Crazy J.
   7. Examples: cat, truth-machine, hello world, quine