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)
W = +(+^)(*0^)

S = ...work in progress...

Note: I'm still brute force searching for short expression for S combinator. The expression for S obtained through BCKW is too long and ugly.

And the other way:

+ =                                  ...work in progress...
* = 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 =                                  ...work in progress...
6 = SSS(S(KS)K)(S(S(KS)K)I)
7 =                                  ...work in progress...
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.

Translation to and from Lazy K

The Church program can be translated into Lazy K program and vice versa (but probably the result of going there and back again would be much larger than the origin).

TODO

Examples

TODO

TODO

1. Add The Church syntax mode to my Lazy K interpreter
2. Publish the interpreter at github (at last)
3. (QUESTIONABLE) Reorder the article parts: start from translation from and to Lazy K, so the language would make an expression of yet another bullshit trivial brainfuck Lazy K substitution. Only then show LC expressions for combinators, reveal their Church numeral nature and explain the name of the language.
4. Find S in The Church basis
5. Find +, 5 and 7 in SKI basis. (Well, there's no need to "find" them, I can just synthesize them using ordinary SKI abstraction elimination rules. Brute force search can yield shorter expressions though)