SKR
| Paradigm(s) | Functional |
|---|---|
| Designed by | User:Hakerh400 |
| Appeared in | 2024 |
| Computational class | Turing complete |
| Major implementations | Implemented |
| File extension(s) | .txt |
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.