SKR

SKR is an esolang invented by User:Hakerh400 in 2024.
== Overview ==
SKR is a purely functional Turing tarpit based on combinatory logic. There are 3 combinators: K, S, R, and the following rewriting rules:
 K x y ---> x
 S x y z ---> x z (y z)
 R x K ---> x K
 R x S ---> x K
 R x R ---> x K
 R x (y z) ---> x S y z
In the last rule, the expression y z must be a WHNF (weak head normal form). A WHNF is one of: K, K x, R, R x, S, S x, S x y, for any expressions x and y (x and y do not need to be WHNFs).
== Syntax ==
Source code consists of definitions. A definition starts with an identifier, then equals sign =, and finally the expression. The last definition in the source code represents the main function. It is called with the input as argument and the result is the output. Definition cannot reference itself, only the definitions before it.
Expression syntax supports the # operator. It represents the low-precedence right-associative application operator. For example, a # b # c d is a (b (c d)).
== Features ==
The unique feature that this language provides is the ability to fully introspect expressions in the language itself. Unlike in the standard SKI calculus, SKR provides a mechanism to analyze expressions without evaluating them.
== Examples ==
Some useful functions:
 I = S K K
 B = S (K S) K
 BB = B B
 C = S (BB S) # K K
 BC = B C
 W = C S I
 T = K
 F = K I
 app_fst = R # K T
 app_snd = R # K F
 fst = B app_snd app_fst
 snd = app_snd
 B2 = BB B
 B3 = BB B2
 B4 = BB B3
 B5 = BB B4
 B2' = B BC # B2 BB B
 B2x = B3 W B2'
 CI = C I
 CI2 = BC CI
 CI3 = B2 C CI2
 W3' = C (B S W) I
 I2 = W I
 I3 = W3' I
 K2 = B K K
 K3 = B K K2
 C2 = BC BC
 C3 = BC # B C2
 C4 = BC # B C3
 C5 = BC # B C4
 C2' = B2 C C
 C3' = B2 C2' C
 C4' = B2 C3' C
 C5' = B2 C4' C
 S2 = I2 # B S
 W2 = B2 W # B W BC
 Bhfxy = B W # B2 C # B (B2 B) B
 Bhfxyzr = B W # B2 C2 # B2 (B2 B2) B2
 pair_cs = C (B S # C B fst) snd
 pair_rd = B3 pair_cs B2'
 swap = pair_cs # C S
 not = C (CI F) T
 or = CI T
 and = C C F
 iff = C S not
 xor = B2 not iff
 xor3 = W B2 xor
 or_and = C2 (B2 B2 # B2 or and) and
 or_and3 = C4 (B4 B2 # B4 or or_and) and
 at_least_2 = B2 W # B W # B2 C # W # BC or_and3
 is_K_or_R' = CI3 I F K
 is_S' = B not is_K_or_R'
 is_K_aux = C2' (W3' S) K I
 is_R_aux = B not is_K_aux
 and' = B2x and
 is_KR_aux = and' is_K_or_R'
 is_K' = is_KR_aux is_K_aux
 is_R' = is_KR_aux is_R_aux
 is_comb = R # C (C is_K' T) # K2 F
 is_app = B not is_comb
 and_safe = C2 (B2 S # C2 C2' # K F) I
 andf = W # BC # B2 B # B and
 is_comb_aux = and_safe is_comb
 is_K = is_comb_aux is_K'
 is_S = is_comb_aux is_S'
 is_R = is_comb_aux is_R'
 cs_comb = C (B B2 # B S # C is_K) # C2' is_S
 cs_app = B R K
 cs_aux1 = B3 K cs_comb
 cs_aux2 = K3 cs_app
 cs = C4 (B4 S # C4' # C2' is_comb cs_aux1 cs_aux2) I
 cs3 = W3' cs
 rec_app = B2 cs_app # S (BC # B BC # B2 (B S) # C # B S BC) I
 rec_aux1 = K # B3 K cs_comb
 rec_aux2 = C4 (B4 S # B4 (B rec_app) I2) I
 rec_r = C5 (B5 S # C5' # C2' is_comb rec_aux1 rec_aux2) I
 rec = I2 rec_r
 rec3 = W3' rec
 eq = rec is_K is_S is_R # K2 # B2 (cs3 F) # B2' and
 ne = B2 not eq
 cs2_fn' = B2 C # B (S I # B C2) B2
 cs2_fn = C (B B cs2_fn') BC
 pair_cs2 = cs2_fn pair_cs
 mk_fn' = BC # B2 I2 # B2 (B2 W) # C (B B # C C4' # K K) # C # B B2 I2
 mk_fn = mk_fn' is_R
 nat_b0 = S (C is_K K) # S K
 nat_b1 = S S
 nat_b = C2' I nat_b1 nat_b0
 0 = K
 1 = nat_b1 0
 nat_cs_aux = B (C2' is_K) # B K # C2' I F 0
 nat_cs = B W # S nat_cs_aux # B pair_cs # C B is_S
 nat_csz = B2 W # C (B (C3' is_K) K2) nat_cs
 nat_cs2 = cs2_fn nat_cs
 nat_op_c_nz_aux1 = B # S # B S2 # B (B2 B2) # B (B2 nat_b) xor3
 nat_op_c_nz_aux2 = B nat_op_c_nz_aux1 # C # B B # B B2 I2
 nat_op_c_nz = B (B2 nat_cs2) nat_op_c_nz_aux2
 nat_op_c_aux = C4' (B C4' # andf is_K) # K # B K2 # C2' I 1 0
 nat_op_c = B I2 # B (B2 W2) # B nat_op_c_aux nat_op_c_nz
 nat_op = C nat_op_c F
 nat_add = nat_op at_least_2
 nat_succ = nat_add 1
 nat_subt' = nat_op # C3' I and or
 nat_le = B (S eq) # S (B B nat_add) # C nat_subt'
 nat_lt = S2 (B2 and nat_le) # B2 not eq
 nat_ge = C nat_le
 nat_gt = C nat_lt
 nat_subt = W2 # C2 (C2 nat_ge nat_subt') # K2 0
 2 = nat_succ 1; 3 = nat_succ 2; 4 = nat_succ 3
 5 = nat_succ 4; 6 = nat_succ 5; 7 = nat_succ 6
 8 = nat_succ 7; 9 = nat_succ 8; 10 = nat_succ 9
 nat_mul_nz_aux = B # S # BC # B2 B # C (B (C2' I) nat_add) I
 nat_mul_nz = B2 nat_cs # nat_mul_nz_aux # C (B B I2) nat_b0
 nat_mul = I2 # B2 W # C4' is_K (K3 0) nat_mul_nz
 nat_snoc = B nat_add # nat_mul 10
 nat = mk_fn 0 nat_snoc
 nat_min = W2 nat_le
 nat_max = W2 nat_ge
 int_aux = C2' # B (Bhfxy S) # C nat_subt
 int' = S2 int_aux nat_min
 int_op = B pair_cs2 # Bhfxyzr int'
 int_add = int_op nat_add
 int_neg = swap
 int_sub = C (B B int_add) int_neg
 nat_to_int = C int' 0
 int0 = nat_to_int 0
 int_snoc = C # B pair_cs # B2 S # C nat_snoc
 int = mk_fn int0 int_snoc
 int_mul_aux1 = Bhfxyzr nat_add nat_mul
 int_mul_aux2 = S2 # B2 S2 # B2 (B2 int') int_mul_aux1
 int_mul = pair_cs2 # int_mul_aux2 # B C2 int_mul_aux1
 nat_inc = nat_succ
 nat_dec = C nat_subt 1
 nat_rec_nz = B2 (S2 I) I2
 nat_rec_aux = C3 (B3 B nat_rec_nz) nat_dec
 nat_rec = I2 # B3 W # C5' is_K (K K2) nat_rec_aux
 nat_iter = C (B B nat_rec) K
 nat_pow = B (nat_iter 1) nat_mul
 cnt' = C (S (S (B rec # CI K) # CI S) # CI R) # K2 nat_add
 cnt = B cnt' # C2' C2' 1 0
 list_rec_nz = B2 (B pair_cs) # B2 (S # BC # B S) I2
 list_rec = I2 # B3 W # C5' is_K (K K2) list_rec_nz
 foldr = C (B B list_rec) # B K
 nat_sum = foldr 0 nat_add
 nat_prod = foldr 1 nat_mul
 foldl = C (B B2 CI) # B (C # C # foldr I) # B2 (C B) C
 sngl = C S K
 snoc = C2' (B foldr sngl) S
 list' = C2' mk_fn' K snoc
 list = list' is_R
 reverse = foldl K # C S
 append = C2' foldr S
As an example, we can use the above functions to check which combinator appears most frequently in the input:
 fn' = B S # B2 S # S (B C # B2 B nat_ge) # C2' (B C2' nat_ge) K R
 fn = C fn' # C2' (B C2' nat_ge) S R
 main = B (S (S (B fn # CI is_K) # CI is_S) # CI is_R) # C cnt
This program outputs the combinator that appears the maximum number of times in the input. If the input is S (S (R # K R) # S R # S S) # R # K # K # K # K # R R, the output will be R. Note that the combinator count is examined in the context of fully evaluated input expression.
== Implementation ==
* Implementation in Haskell
Category:Languages
Category:2024
Category:Turing complete
Category:Functional paradigm
Category:Implemented