15
\$\begingroup\$

This challenge is to golf an implementation of SKI formal combinator calculus.

Definition

Terms

S, K, and I are terms.

If x and y are terms then (xy) is a term.

Evaluation

The following three steps will be repeated until none of them apply. In these, x, y, and z must be terms.

(Ix) will be replaced by x

((Kx)y) will be replaced by x

(((Sx)y)z) will be replaced by ((xz)(yz))

Input

A string or array, you do not have to parse the strings in the program.

The input is assumed to be a term.

If the simplification does not terminate, the program should not terminate.

Examples

(((SI)I)K) should evaluate to (KK) ((((SI)I)K) > ((IK)(IK)) > (K(IK)) > (KK))

The evaluation order is up to you.

This is . Shortest program in bytes wins.

\$\endgroup\$
17
  • 2
    \$\begingroup\$ Are the inputs strings we have to parse, or can we have them in a tree or similar? \$\endgroup\$
    – xnor
    Jun 8, 2020 at 21:03
  • 5
    \$\begingroup\$ Some example please. \$\endgroup\$
    – Noodle9
    Jun 8, 2020 at 21:27
  • 1
    \$\begingroup\$ Should we assume the input is a term (i.e. the behavior is unspecified if the input is not a term)? Is a non-strict evaluation order required so that ((KI)(((SI)I)((SI)I))) must terminate, or is such an expression allowed to diverge? \$\endgroup\$ Jun 8, 2020 at 22:53
  • 4
    \$\begingroup\$ @nph The point is that ((KI)(((SI)I)((SI)I))) can either be reduced to I with one K step (leading to termination) or to ((KI)(((SI)I)((SI)I))) with one S step (leading to divergence), and you need to specify whether the former is required, the latter is required, or either are allowed. I suggest “either”. See en.wikipedia.org/wiki/Evaluation_strategy. \$\endgroup\$ Jun 8, 2020 at 23:23
  • 2
    \$\begingroup\$ @user Outputting a function would give you no way to distinguish between terms like I and ((SK)K), which behave the same way as functions but are different formal terms according to the specification. \$\endgroup\$ Aug 24, 2020 at 21:53

13 Answers 13

14
\$\begingroup\$

Seed, 5925 5909 5890 5871 bytes

112 15005947709794001551745957934844387741963949195277224222942941175436326514584950738591687605839219554765312673139412565708303623220949435523970322376797353146959745711905510018709836078812043106050834210308953675588904375331147958460963516014023707270232815615580191475313492822637836797632954281710946191499605228074932238550384395938117947060215994891322895044239528628512342238908241756883576002309136458318426853695392342134155539648665540277527361486373315204318620925711966035942972301024071758707541614676997726343666069365960926312389921620411476834005712809293274727572041778318193400305675046336765396855687333907497840274069746276373367369703580554409090562378751245676511475863473197371503596617476237367564859524783860932491719480838743775854752937582631478472858805293525550579186499439467601324049079649702705638149237726903715713198300458483396210318594205002535699020033101313998794049241761482893215545820063264328229881143576843458089686528082309939218920676760397200190753211539050612871378253300234981486827195149285993539318712648895148239989077967469145906695695725639268359301194662154392742578020810701834214158736314590623136502888397978749532810617946493901929092720143858186563905545327303571180219726465764878181781793186557115346627825930278330900621009385247050349799814637325838873386273620292889508639528760077557546022550893317195975075676364661558122052118325128379943533068090012220829021399689156629396236283055797200153622175538248583908589003663439918426202812570956934037616313978141038436250235826227599001867803787753289942830662970049826887648134355967676874394598303565162564098091962321618997451086001894320616183844450949745111961097935961422054551097993708497261609312619851867552774875820025258452120004909524068566821412865560838149303210060349938961761533503092020673002416898086436041943447125182745611224019177109739446600864677559430466121929945756146084077508406141217714924746215384101090025498044684775465393706427360635410805944030744216263012281416728398396416831795019051695841375796012411932982781478577883259595757903277557013560339885004421095676988158159396051716905851695868846217163033650855582743560777135998979147462531018626808123024651044752899172971002767697839239729810707234489951369936874749971224648800779627289820691653942304035510887312581099887291489063786961615815819042632926041887143023442493367191018860931124256737065291117513395597390330436919578761534024220110023138771538795599121937519406552355650683399790256516607065531496732816853693448215404786400970519966206258869445999493937332453168572772112997760870010241144983948646532970556412494478470874278789858188343190563017173944011190771623840595351509754982449024750394701519531006485472627145366830956667859501091417380696397464590991791308983349002274205858210760481683412352685066760822807899782234565255719233842430215301267239587428773746177871165689901600646208417243654576703937071967370788826253003884731359674397195313538272303293175867053889097207394492875065268350307339622671904542995950940807603665603392360313488803906413379430184051083670651885004729854473727892899327473728338289015477022005098264171173287148216655347470405522687318205669926969047603404427022940081372422043277056357622857655043121570602934088962243851150034231358205417695570313960867608351649616601597171103712920006771227684820533564475176054040787432340472274329195572428023594055583381411302879259043579364074516131781566192239762614111449269891788954603213847889168431350014116352332568495719218713235740892206829549462198325993188837102069283539752183758065423840683800603399859637684399037099221818564860203439420354868316030912624198686770619813926501773589831388435439912756367101921385867304769841318242527202174699712749989890549100618766195763093033777895223312002305430160001275541120625668816562872370554533240740711308545492566622447387847129184675258840061167986941835187326795163219815464893135818120045226688158342762111189020715287040929632731150621861797218443116943858771703314057252808040194719272221568604757655663698552989990229004273536247930781680140083595248339872510398208349681626516323634002414520180187717671833484137244164128541147709523893558998899056288656978386170358563298472726263463417577850405538930616250768204180320433714120300698104642831290348733321737432889366924916049752215841193779080800636674778497915959708337417182273764342346866774775653756058911256185185873508680869141984524483214089280934429062520714358784586525050484207441645220993262882342756100509032546437508737632994769953343557031259340876734256731175957719696115684088124816754110816835876004771979087627144264947341007701385546122301660045006701955256463852124008422794869017906021119668922855196994038408121927354830095485511684485897883093363153061118792730884544102569938337293922496429629026756031491789824151232745788879429878141955008264934544729922641571626500646801646006325177424332041649880615834179528840475135442387961477263271755349703111900050322015750046110520113769061873773224255260567367037977307039933923712455102299122383393934719598954896540671632062855631877929121978543395229931810235373538276109853789473509980161486544938872377251787271170167749722788024574615673100600339991716767083485020637569393181718479956878303006973117799848008281819831255077962986793387572680394422233339861138992427628320726864707782719207666267011154525035418875867304015403972370212699575463083434809323275089626152829749877006988525385406485549790996313807504116069326092250060019527246837345192885824159103450484754359747938657719239950929657439192593009675109091074171048468653400294437717256292360536782184532950229108298749236074423546534432582236295463728400904674225389451924335046169486189781521045046285871978796304537708669530610470217951827243335780340661190275411840673425107286839355369264896654238856744240956275

Try it online!

Made possible thanks to Abigail's perl answer. Inspired by HighlyRadioactive's comment.

Last iteration was golfed with bx6.

\$\endgroup\$
5
  • 2
    \$\begingroup\$ What the... this is real... \$\endgroup\$ Aug 21, 2020 at 1:17
  • 2
    \$\begingroup\$ Now, do this in Malbolge. \$\endgroup\$
    – user96495
    Aug 22, 2020 at 3:04
  • 1
    \$\begingroup\$ Challenge accepted, but let me finish my work first ;) \$\endgroup\$ Aug 22, 2020 at 9:08
  • \$\begingroup\$ This is wrong for the same reason as user89655’s answer; namely, it fails to simplify, e.g., ((K(SS))S) to (SS). (In the rules, x, y, and z are terms; they don’t have to be single characters.) \$\endgroup\$ Aug 24, 2020 at 7:02
  • 1
    \$\begingroup\$ @AndersKaseorg fixed; it hurt many bytes but should work correctly now. \$\endgroup\$ Aug 24, 2020 at 17:43
11
\$\begingroup\$

C (gcc), 666 616 518 483 476 bytes

Who doesn't love classy, Arthur Whitney-styled code? No regular expressions involved, only clever parsing and evaluation.

PS: Yes, obviously, a few bytes can be shaved off, but for the artistic style of the obfuscated code, I'll keep them. Also for the byte count :p. Also, this code utilizes undefined behaviour in hope that nothing will break (hopefully).

@ceilingcat insisted on golfing it down from 666 bytes, so here is the golfed version:

#define J putchar
#define H O->a
#define G H->a
#define K O->b
typedef struct x{struct x*a,*b;int q;}Y;Y*O;z=1;A(q){O=calloc(6,4);O->q=q;}h(Y*O){Y*u;O=H&&H->q==2?z=K:H&&G&&G->q==1?z=H->b:H&&G&&G->a&&!G->a->q?u=A(3),(u->a=A(3))->a=G->b,(u->b=A(3))->a=H->b,u->a->b=u->b->b=K,z=u:(O->q==3?H=h(H),K=h(K):0,O);}r(x){Y*O;x=getchar()-73;x=x+33?A(x?x!=10:2):!getchar(K=r(H=r(O=A(3))))+O;}q(Y*O){O&&J(O->q["SKI "],O->q-3||J(41,q(K),q(H),J(40)));}main(){Y*O=r();for(;z;O=h(O))z=0;q(O);}

Try it online!

\$\endgroup\$
1
  • 1
    \$\begingroup\$ Now, do this in Seed. \$\endgroup\$ Aug 20, 2020 at 9:09
10
\$\begingroup\$

Wolfram Language, 63 bytes

#//.{{I,x_}->x,{{K,x_},y_}->x,{{{S,x_},y_},z_}->{{x,z},{y,z}}}&

Try it online!

God, I love pattern matching in Wolfram Language. Represents (xy) as {x,y} (a list of two elements).

Alternatively, if we represent (xy) with x>y, we can do it in 55 bytes.

#//.{I>x_->x,(K>x_)>y_->x,((S>x_)>y_)>z_->(x>z)>(y>z)}&

Try it online!

\$\endgroup\$
1
  • 2
    \$\begingroup\$ Basic -1. Alternatively, save more with // instead of >: 45 bytes \$\endgroup\$
    – att
    Aug 25, 2020 at 20:39
5
\$\begingroup\$

Rust Macros, 480 441 bytes

macro_rules!s{({I$($t:tt)+}$s:tt)=>{s![{$($t)+}$s]};({K$x:tt$y:tt$($t:tt)*}$s:tt)=>{s![{$x$($t)*}$s]};({S$x:tt$y:tt$z:tt$($t:tt)*}$s:tt)=>{s![{$x$z($y$z)$($t)*}$s]};({($($c:tt)*)$($t:tt)*}{$($r:tt)*})=>{s![{$($c)*}{{$($t)*}$($r)*}]};({$($c:tt)*}{{$($t:tt)*}$($s:tt)*})=>{s![{$($c)*$($t)*}{$($s)*}]};({$($c:tt)*}{})=>{concat!($(s![$c]),*)};(($($t:tt)*))=>{concat!("(",s!($($t)*),")")};($t:tt)=>{stringify!($t)};($($t:tt)*)=>{s![{$($t)*}{}]};}

Try it online!

The macro takes in tokens and spits out a string literal. Input is in a flattened, left-associative format as seen on Wikipedia. Make sure there is some whitespace between combinators when using it. ungolfed:

macro_rules! ski {
    ({I $($t:tt)+} $s:tt) => {ski![ {$($t)+} $s]};
    ({K $x:tt $y:tt $($t:tt)*} $s:tt) => {ski![ {$x $($t)*}$s] };
    ({S $x:tt $y:tt $z:tt $($t:tt)*} $s:tt) => {ski![ {$x $z ($y $z) $($t)*} $s ]};
    ({($($c:tt)*) $($t:tt)+}{$($r:tt)*}) => {ski![ {$($c)+} {{$($t)*} $($r)*} ]};
    ({$($c:tt)*} { {$($t:tt)*} $($s:tt)* }) =>{ski![ { $($c)* $($t)* } {$($s)*} ]};
    ({$($c:tt)*} {}) => {concat!($(ski![$c]),*)};
    (($($t:tt)*)) => {concat!("(", ski!($($t)*), ")")};
    ( $t:tt) =>{stringify!($t)};
    ($($t:tt)*) => {ski![ {$($t)*} {}]};
}

Macros declared with macro_rules perform substitution based on rules similar to a regex-based substitution. The general strategy is here is an execution stack, where the instructions are being stored and executed, and a call stack, which is a stack of execution stacks and is used to traverse into functions created with ().

Rule number ten serves as the entry point to the macro, matching on all inputs and setting up the call and execution stacks in the form {instructions}{}. Note that matched pairs of brackets count as a single token, and closing brackets stop greedy matches.

Rule one implements the I combinator. It matches when the call stack is I followed by one or more instructions. It simply passes on all the matched instructions.

Rule two implements the K combinator. It behaves similarly to I but uses two arguments instead of one.

Rule three is the same but for S.

Rule four implements traversing into parentheses by pushing the instructions remaining on the execution stack after the parentheses onto the call stack, and replacing the call stack with the instructions in the parentheses.

Rule five catches an edge case by stopping infinite recursion when there are no instructions after the parentheses. was made redundant by an earlier bug fix and removed.

Rule six is when the execution stack can't be simplified and there are more instructions on the call stack, the instructions in the top execution stack on the call stack are concatenated on the bottom of the main execution stack.

Rule seven is when the execution stack can't be simplified and the call stack is empty. Here all the tokens are split, fed back into this macro for stringification, and concatenated.

Rule eight is where I say I lied because parenthesized groups need further evaluation because that strategy I had above evaluated these groups lazily. This rule simply feeds the instructions in the parentheses back into the original macro and concatenates parentheses around the results.

Rule nine is our terminal rule, where the tokens passed in are stringified and returned.

Assuming the recursion limit is removed and rustc gets unlimited memory this is a proof of turing completeness for rust's macro system (not the only one- rust's macros are trivially ℒ-hard, a macro that binds an inputted $ can create and execute arbitrary macros). A playground link that lets you view the ungolfed macro's expansion steps is below.

Playground

\$\endgroup\$
4
+100
\$\begingroup\$

APL (Dyalog Unicode), 127 124 bytes

Full program. No use of regex.

∊{0=≡⍵:⍵
1⌽')(',∇¨⍵}{0=d←|≡⍵:⍵
'I'≡⊃⍵:⊃⌽⍵
(2≤d)∧'K'≡⊃⊃⍵:⊃⌽⊃⍵
(3≤d)∧'S'≡⊃∊⍵:x y,⍥⊂¨⊃⌽(((s x)y)z)←⍵
∇¨⍵}⍣≡⍎⍕{3⍴''''⍵}¨@{⍵∊⎕A}⍞

Try it online!

The program has three distinct parts:

  • Input handling
  • Evaluation
  • Output formatting

Input handling

This part transforms the traditional SKI notation into a nest APL data structure.

      ⍎⍕{3⍴''''⍵}¨@{⍵∊⎕A}⍞

 prompt for one line of input text
  E.g. "(((SI)I)K)"

@{}at locations where:

 the argument characters

 are members of

⎕A the uppercase Alphabet

{ replace each one by:

3⍴ a cyclical reshape into length 3, of

''''⍵ the string consisting of a quote character (') and the argument character
  E.g. ["(","(","(","'S'","'I'",")","'I'",")","'K'",")"]

 stringify (this forces the now nested array into a flat space-separated string)
  E.g. "((( 'S' 'I' ) 'I' ) 'K' )"

 evaluate as APL code
  E.g. [["SI","I"],"K"]

Evaluation

This part simplifies the data structure according to the three given rules.

           {0=d←|≡⍵:⍵
'I'≡⊃⍵:⊃⌽⍵
(2≤d)∧'K'≡⊃⊃⍵:⊃⌽⊃⍵
(3≤d)∧'S'≡⊃∊⍵:x y,⍥⊂¨⊃⌽(((s x)y)z)←⍵
∇¨⍵}

0=: if 0 equals
d← the variable d which is (assigned for later use)
|≡⍵ the absolute depth (maximum nesting level) of the argument:

 return the argument as-is (this ensures the continuation of already evaluated parts)

'I'≡: if "I" matches
⊃⍵ the first element of the argument

⊃⌽⍵ return the last element of the argument (lit. the first of the reversed; this implements (Ix)x)

(2≤d)∧: if 2 is less than or equal to the depth (d), AND
'K'≡⊃⊃⍵ if "K" matches the first element of the first element of the argument:

⊃⌽⊃⍵ return the last element of the first element of the argument (lit. the first of the reversed first; this implements ((Kx)y)x)

(3≤d)∧: if 3 is less than or equal to the depth (d), AND
'S'≡ if "S" matches
⊃∊⍵ the first element of the enlisted (flattened) argument:

(((s x)y)z)←⍵ destructure the argument into individual variables
⊃⌽ pick the last element (lit. first of the reversed) from that (z)
x y,⍥⊂¨ pair up each of x and y with that (this implements (((Sx)y)z)((xz)(yz)))

∇¨⍵ otherwise, call self on each element of the argument

Output Formatting

Here, we transform the data structure back into traditional SKI notation.

∊{0=≡⍵:⍵
1⌽')(',∇¨⍵}

0=≡⍵: if zero is equal to the depth of the argument (i.e. it is a single character)

 return that as-is

∇¨⍵ otherwise, call self on each element of the argument
')(', prepend ")("
1⌽ cyclically rotate one character from the front to the rear.

\$\endgroup\$
3
\$\begingroup\$

perl -p, 135 bytes

1 while s/\((I)(?<T>[SKI]|\((?&T)(?&T)\))\)|\(\((K)((?&T))\)(?&T)\)|\(\(\((S)((?&T))\)((?&T))\)((?&T))\)/$1?$2:$3?$4:"(($6$8)($7$8))"/e

Try it online!

Just a regexp applying the three rules. Reads a string from STDIN, applies all the rules until there's nothing to apply, writes the result to STDOUT.

(?<T>[SKI]|\((?&T)(?&T)\)) is a recursive pattern recognizing a term. The rest of the pattern is just a mechanically translation of the given rules.

\$\endgroup\$
2
3
\$\begingroup\$

Retina 0.8.2, 171 bytes

{T`()`<>
<<<S((\w|(<)|(?<-3>>))+)>((\w|(<)|(?<-6>>))+)>((\w|(<)|(?<-9>>))+>)
<<$1$7<$4$7>
<<K((\w|(<)|(?<-3>>))+)>(\w|(<)|(?<-5>>))+>
$1
<I((\w|(<)|(?<-3>>))+)>
$1
T`<>`()

Try it online! Explanation:

{`

Repeat the transformations until there are no more available.

T`()`<>
T`<>`()

Temporarily switch ()s with <>s to avoid having to quote numerous ()s.

<<<S((\w|(<)|(?<-3>>))+)>((\w|(<)|(?<-6>>))+)>((\w|(<)|(?<-9>>))+>)
<<$1$7<$4$7>

Process S operations. (The last capture includes the trailing > in order to avoid repeating it in the replacement.)

<<K((\w|(<)|(?<-3>>))+)>(\w|(<)|(?<-5>>))+>
$1

Process K operations.

<I((\w|(<)|(?<-3>>))+)>
$1

Process I operations.

The (\w|(<)|(?<-[N]>>))+ construct is an example of a .NET regex balancing group. It tries to match characters, but it's only allowed to match >s if it's already seen the same number of <s. (N needs to be replaced with the number of the (<) capturing group. As written it fails if the <>s aren't balanced correctly, but you can use conditional regex to check for that.)

\$\endgroup\$
3
\$\begingroup\$

Wolfram Language, 44 bytes

s[a_][b_][c_]:=b@c//a@c;k[a_][b_]:=a;i@a_:=a

This defines them as actual functions in Wolfram, so s[i][i][k] returns k[k], etc.

Try it online!

\$\endgroup\$
1
  • 5
    \$\begingroup\$ -6 bytes \$\endgroup\$
    – att
    Aug 29, 2021 at 6:02
2
\$\begingroup\$

05AB1E, 92 bytes

ΔDŒʒ„)(©S¢Ë}ʒÁ®Å?y®S¢O_~}©vy"(Iÿ)"y:}®ãvy`"((Kÿ)ÿ)"yθ:}®3ãvy`"(((Sÿ)ÿ)ÿ)"yĆ1.I`"((ÿÿ)(ÿÿ))":

05AB1E has no regex, so uses a brute-force approach using all valid substrings. Because of this, it's extremely slow for larger test cases.

Executes in the order (Ix)((Kx)y)(((Sx)y)z).

Try it online or verify a few more test cases.

Explanation:

Δ                        # Continue until the result no longer changes:
 D                       #  Duplicate the current string
                         #  (will use the implicit input-string in the first iteration)
  Π                     #  Take all its substrings
   ʒ                     #  Filter those substrings by:
    „)(                  #   Push ")("
       ©                 #   Store it in variable `®` (without popping)
        S                #   Convert it to a list of characters: [")","("]
         ¢               #   Count each in the substring
          Ë              #   Check that the counts are equal for both
   }ʒ                    #  After the filter: filter once more:
     Á                   #   Rotate the substring once towards the left
      ®                  #   Push string ")(" from variable `®`
       Å?                #   Check if the rotated substring starts with this
     y                   #   Push the substring again
      ®S¢                #   Count the [")","("] again
         O_              #   Check that the sum of both counts is 0
     ~                   #   Check if either of the two was truthy
    }©                   #  After the filter: store it in variable `®` (without popping)
 v                       #  Loop over each valid substring:
  y                      #   Push the substring
   "(Iÿ)"                #   Push this string, with the `ÿ` automatically filled with
                         #   the substring
  y                      #   Push the substring again
  :                      #   Replace all "(Ia)" with "a"
 }®                      #  After the loop: push the list of valid substrings again
   ã                     #  Take all pairs of valid substrings
    v                    #  Loop over these pairs:
     y`                  #   Pop and push the pair separated to the stack
       "((Kÿ)ÿ)"         #   Push this string, with the `ÿ` automatically filled again
     yθ                  #   Pop and push only the last substring of the pair: [a,b] → b
     :                   #   Replace all "((Kb)a)" with "b"
 }®                      #  After the loop: push the list of valid substrings again
   3ã                    #  Take all triplets of valid substrings this time
     v                   #  Loop each each triplet:
      y`                 #   Pop and push the triplet separated to the stack
        "(((Sÿ)ÿ)ÿ)"     #   Push this string, with the `ÿ` automatically filled again
      y                  #   Push the current triplet again
       Ć                 #   Enclose; append its own head: [a,b,c] → [a,b,c,a]
        1.I              #   Get the 0-based 1st permutation: [a,b,c,a] → [a,b,a,c]
           `             #   Pop and push the quartet separated to the stack
            "((ÿÿ)(ÿÿ))" #   Push this string, with the `ÿ` automatically filled again
      :                  #   Replace all "(((Sc)b)a)" with "((ca)(ba))"
                         # (after which the result is output implicitly)
\$\endgroup\$
2
\$\begingroup\$

Scala 3 (compile-time), 113 bytes

type A=AnyKind
type S[X[a<:A]<:[b<:A]=>>A]=[Y[z<:A]]=>>[Z<:A]=>>X[Z][Y[Z]]
type K[X<:A]=[Y<:A]=>>X
type I[X<:A]=X

Try it in Scastie

It works at compile time and it doesn't exactly return a value (you can check it with =:= or other mechanisms), but Dotty's type system is Turing-complete (Scala 2's too, actually).

Pretty straightforward - it uses higher-kinded types and curried type lambdas like functions.

Ungolfed (and modified slightly for clarity):

type S = 
  [X <: [a <: AnyKind] =>> [b <: AnyKind] =>> AnyKind] =>> //X is a type lambda with 2 parameters (curried) and returning a type of any kind
  [Y[z <: AnyKind]] =>> //Y is a type lambda taking one parameter and returning a type of any kind
  [Z <: AnyKind] //Z is a type of any kind
  =>> X[Z][Y[Z]] //The result of Skyz, as defined in the question
type K = [X <: AnyKind] =>> [Y <: AnyKind] =>> X
type I = [X <: AnyKind] =>> X

SIIK or (((SI)I)K) would be written as S[I][I][K].


With match types, 200 bytes

final class S
final class K
final class I
type R[T]=T match{case(((S,x),y),z)=>R[((x,z),(y,z))]case((K,x),y)=>R[x]case(I,x)=>R[x]case(a,b)=>R[a]match{case`a`=>(a,R[b])case _=>R[(R[a],R[b])]}case T=>T}

Thanks to @HTNW on SO for helping me with this

Try it in Scastie

A term (xy) is represented as the tuple (x,y).


Using literal types, 164 bytes

type R[T]=T match{case((('S',x),y),z)=>R[((x,z),(y,z))]case(('K',x),y)=>R[x]case('I',x)=>R[x]case(a,b)=>R[a]match{case`a`=>(a,R[b])case _=>R[(R[a],R[b])]}case T=>T}

Try it in Scastie

This one uses literal-based singleton types (the Chars 'S', 'K', and 'I').


Slightly unethical version, 158 bytes

type R[T]=T match{case(((0,x),y),z)=>R[((x,z),(y,z))]case((1,x),y)=>R[x]case(2,x)=>R[x]case(a,b)=>R[a]match{case`a`=>(a,R[b])case _=>R[(R[a],R[b])]}case T=>T}

Same approach as above, but this time, S is the singleton type of 0, K is 1, and I is 2.

Try it in Scastie

\$\endgroup\$
2
\$\begingroup\$

KamilaLisp, 137 bytes

(defmacro f(x)(match x((a b c)(S a b c)[(tie a c b c)/ 2])((a b)(K a b)a)(a(I a)a)((a b)(a b)(tie(f a)(f b)))(x)))(def g $(iterate /= f))

Ungolfed:

;; SKI calculus implementation using KamilaLisp macros
(defmacro ski (x) (match x
    ((a b c) (S a b c) [(tie a c b c) / 2])
    ((a b)   (K a b)   a)
    ((a)     (I a)     a)
    ((a b)   (a b)     (tie (ski a) (ski b)))
    (x)
))

;; iterate /=  =>  fixed point
(def ski-red $(iterate /= ski))

;; an example expression
(println@ski-red '(S I I K))
\$\endgroup\$
2
\$\begingroup\$

Maude, 138 bytes

fmod F is
sort T .
ops S K I : -> T .
op __ : T T -> T .
vars x y z : T .
eq I x = x .
eq (K x)y = x x .
eq ((S x)y)z = (x z)(y z) .
endfm
Maude> red ((S I)I)K .
reduce in F : ((S I) I) K .
rewrites: 3 in 0ms cpu (0ms real) (~ rewrites/second)
result T: K K
\$\endgroup\$
1
\$\begingroup\$

Haskell, 83 bytes

data T=S|K|I|T:$T
e(x:$y)=e x!e y
e x=x
I!x=x
K:$x!_=x
S:$x:$y!z=x!z!(y!z)
x!y=x:$y

Try it online!

\$\endgroup\$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.