# SKI Combinators Redux

On this page we look at the redux function for SKI Combinators. This follows on from the introduction to SKI Combinators on this page.

## Tutorial

If you are working with a version of FriCAS before 1.1.3 then the Ski domain needs to be installed on your system as described on this page.

On this page we will be working with 'untyped' SKI combinators so we create an instance called UNTYP to simplify notation:

 ```(1) -> UNTYP := SKICombinators Untyped (1) SKICombinators(Untyped) Type: Type```

### SKI Combinator Redux

We will check that the program agrees with the following known results:

• SIKx ⊳ Ix(Kx) ⊳ x(Kx)
• SSKxy ⊳ xy(Kxy) ⊳ xyx
• S(SK)xy ⊳ SKy(xy) ⊳ K(xy)(y(xy)) ⊳ xy
• S(KS)Sxyz ⊳ KSx(Sx)yz ⊳ Sxz(yz) ⊳ x(yz)(z(yz))
• S(S(KS)K)(S(KS)K)Ixy ⊳ S(KS)KI(S(KS)KI)xy ⊳ KSI(KI)(KSI(KI))xy ⊳ KIx(S(KI)x)y KIy(xy) ⊳ xy

When we do this with the program we get:

SIKx ⊳ Ix(Kx) ⊳ x(Kx)

 ```(2) -> s1 := parseSki("SIKx")\$UNTYP (2) SIK x Type: SKICombinators(Untyped) (3) -> redux(s1)\$UNTYP I x(K x) x(K x) (3) x(K x) Type: SKICombinators(Untyped)```

SSKxy ⊳ xy(Kxy) ⊳ xyx

 ```(4) -> s2 := parseSki("SSKx y")\$UNTYP (4) SSK x y Type: SKICombinators(Untyped) (5) -> redux(s2)\$UNTYP x y(K x y) x y x (5) x y x Type: SKICombinators(Untyped) ```

S(SK)xy ⊳ SKy(xy) ⊳ K(xy)(y(xy)) ⊳ xy

 ```(6) -> s3 := parseSki("S(SK)x y")\$UNTYP (6) S(SK) x y Type: SKICombinators(Untyped) (7) -> redux(s3)\$UNTYP SK y(x y) K(x y)(y(x y)) x y (7) x y Type: SKICombinators(Untyped) ```

S(KS)Sxyz ⊳ KSx(Sx)yz ⊳ Sxz(yz) ⊳ x(yz)(z(yz))

 ```(8) -> s4 := parseSki("S(KS)Sx y z")\$UNTYP (8) S(KS)S x y z Type: SKICombinators(Untyped) (9) -> redux(s4)\$UNTYP KS x(S x) y z S x z(y z) x(y z)(z(y z)) (9) x(y z)(z(y z)) Type: SKICombinators(Untyped) ```

S(S(KS)K)(S(KS)K)Ixy ⊳ S(KS)KI(S(KS)KI)xy ⊳ KSI(KI)(KSI(KI))xy ⊳ KIx(S(KI)x)y KIy(xy) ⊳ xy

 ```(10) -> s5 := parseSki("S(S(KS)K)(S(KS)K)Ix y")\$UNTYP (10) S(S(KS)K)(S(KS)K)I x y Type: SKICombinators(Untyped) (11) -> redux(s5)\$UNTYP S(KS)KI(S(KS)KI) x y KSI(KI)(KSI(KI)) x y KI x(S(KI) x) y KI y(x y) x y (11) x y Type: SKICombinators(Untyped)```

## Modeling Computation

 metadata block see also: Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.