{"id":11,"date":"2016-01-25T19:35:36","date_gmt":"2016-01-25T19:35:36","guid":{"rendered":"http:\/\/143.198.247.44\/wordpress\/?p=11"},"modified":"2024-10-04T16:34:45","modified_gmt":"2024-10-04T16:34:45","slug":"skiing-with-y-iota-and-ackermann","status":"publish","type":"post","link":"https:\/\/www.type.sh\/index.php\/2016\/01\/25\/skiing-with-y-iota-and-ackermann\/","title":{"rendered":"SKIing with Y*, Iota and Ackermann"},"content":{"rendered":"

(Source code for this post is here: https:\/\/github.com\/mikebern\/lambda_ski_iota<\/a>\u00a0)<\/p>\n

There are only six atomic operations for Turing machines – read and write to the tape, move the tape left or right one square,\u00a0\u00a0change state based on the observed symbol and halt. Yet,\u00a0it’s not hard to see, at least at a high level, how a program in an imperative language such as C or Fortran would be translated to a program for a Turing machine – variables are cells on the tape, operations are modifications of those cells and control structures move the tape according to the specified conditions. \u00a0This connection becomes much less obvious for functional programming languages such as Lisp or Haskell, and indeed they are based on another computation paradigm – lambda calculus.<\/p>\n

Lambda calculus actually predated Turing machines. The first paper on the former was published in 1932, while on the latter in 1937. \u00a0It is deemed impossible to directly compare their computation powers, but Church-Turing thesis<\/em>\u00a0postulates that they are able to compute exactly the same class of functions, called computable functions<\/em>. \u00a0Both lambda calculus and Turing machines had inspired creation of high-level programming languages, the first being Fortran followed by Lisp with a gap between the two of less than a year.<\/p>\n

So the question arises – what is the ‘assembly language’ for the functional languages? The answer is quite surprising – using only 3 combinators<\/em>\u00a0– S<\/strong>, K<\/strong>, I<\/strong> we can express any lambda function. This system is called SKI-calculus<\/a>\u00a0. Sometimes it is written as SK(I)<\/strong> or to emphasize that\u00a0I<\/strong> can be easily expressed using S<\/strong> and K<\/strong> (I =(S K K)<\/strong>).<\/em> Can we do better than 2 combinators? \u00a0Yes! All three can be expressed with only one function called X<\/strong><\/a><\/em>! There are actually quite a few versions of X<\/strong>. The one that we use here has its own name – Iota<\/em> (see\u00a0Wikipedia<\/a>). For other versions see Fokker, The systematic construction of a one-combinator basis<\/a>, there is also Hankin X<\/strong> combinator, described in his book Lambda Calculi, A Guide for Computer Scientists<\/a> on p. 61.<\/p>\n

It follows that all algorithms can be written using just\u00a0X<\/strong>\u00a0and parentheses. For instance,\u00a0<\/p>\n

\nQuick Sort in SKI<\/strong> calculus<\/summary>\n


\n((S (K (S I I)) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S I I)))))) (K (K I)))) (S (K (S (S (S (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) (S (K (S (K (S I (K (S (K K) I)))) I)) I)) (K (((S (S (K S) (S (K K) (S (K S) (S (K (S I)) (S (K K) I))))) (K (S (K K) I))) (S (K K) I)) (S (K K) I)))))) (S (S (K S) (S (K (S (K (S (K (S (S (K ((S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (K (S (K (S (K (S I I)) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S I I)))))) (K (K I))))))) (S (K (S (S (K S) (S (K K) (S (K S) (S (K (S (S (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) (S (K (S (K (S I (K (S (K K) I)))) I)) I)))) (S (K K) I))))))) (S (K K) (S (S (K S) (S (K K) (S (K S) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I (K (S (K K) I)))) (S (K (S I (K (K I)))) I))) I)))))) (K (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I (K (K I)))) (S (K (S I (K (K I)))) I))) I))))))))))) (K (K I))) (S (K (S (K ((S (S (K S) (S (K K) (S (K S) (S (K (S I)) (S (K K) I))))) (K (S (K K) I))) (K I))))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K K) (S (K S) (S (K (S I)) (S (K K) I))))) (K (S (K K) I)))) I))) (K I))))) I))) (S (K K) I))))) (S (S (K S) (S (K K) I)) (K (S (S (K (S (S (K S) (S (K K) (S (K (S (K (S I I)) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S I I)))))) (K (K I))))) (S (K (S (K (S (S (S (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) (S (K (S (K (S I (K (S (K K) I)))) I)) I)) (K (((S (S (K S) (S (K K) (S (K S) (S (K (S I)) (S (K K) I))))) (K (S (K K) I))) (S (K K) I)) (S (K K) I)))))))) (S (S (K S) (S (K (S (K S))) (S (S (K S) (S (K K) (S (K S) (S (K (S (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))))) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I (K (S (K K) I)))) (S (K (S I (K (K I)))) I))) I))))))) (K (S (K (S (S (K (S (K (S (K ((S (S (K S) (S (K K) (S (K S) (S (K (S I)) (S (K K) I))))) (K (S (K K) I))) (K I))))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K K) (S (K S) (S (K (S I)) (S (K K) I))))) (K (S (K K) I)))) I))) (K I)))) (S (K (S (K (S I (K (S (K K) I)))) (S (K (S I (K (K I)))) I))) I)))) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I (K (K I)))) (S (K (S I (K (K I)))) I))) I)))))))) (K (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I (K (K I)))) (S (K (S I (K (K I)))) I))) I))))))))) (K I))) (S (K (S (S (K (S (S (K S) (S (K (S (K (S (S (K S) (S (S (K S) (S (K K) I)) (K I))) (S (K K) I))))) (S (S (K S) (S (K K) (S (K (S (K (S (K (S (S I (K (K (K I)))) (K (S (K K) I)))))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K S))) (S (K (S (K (S (K S))))) (S (K (S (K (S (K K))))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (K (S (S I (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K S))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I)))) (S (K (S (K K))) (S (K (S I)) (S (K K) I))))))))) (K (K (S (K K) I)))))) (K (K (K I))))) I))) (K I))))) (K (K I))))))) (S (K K) I))))) (K (K I))))))) (K (K (K I))))) I))) (K I)))) I))) (K I)))) (S (K (S (K (S (S I (K (K I))) (K (S (K K) I)))))) (S (K (S (S (K (S (S (K S) (S (K (S (K (S (S (K S) (S (S (K S) (S (K K) I)) (K I))) (S (K K) I))))) (S (S (K S) (S (K K) (S (K (S (K (S (K (S (S I (K (K (K I)))) (K (S (K K) I)))))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K S))) (S (K (S (K (S (K S))))) (S (K (S (K (S (K K))))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (K (S (S I (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K S))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I)))) (S (K (S (K K))) (S (K (S I)) (S (K K) I))))))))) (K (K (S (K K) I)))))) (K (K (K I))))) I))) (K I))))) (K (K I))))))) (S (K K) I))))) (K (K I))))))) (K (K (K I))))) I))) (K I)))) I))) (K I)))) (S (K (S (S (K (S (K (S (K (S (S I (K (K (K I)))) (K (S (K K) I)))))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K S))) (S (K (S (K (S (K S))))) (S (K (S (K (S (K K))))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (K (S (S I (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K S))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I)))) (S (K (S (K K))) (S (K (S I)) (S (K K) I))))))))) (K (K (S (K K) I)))))) (K (K (K I))))) I))) (K I))))) (K (K I))))))) (S (K K) I))))) (K (K I))))))) (K (K (K I))))) I))) (K I)))) I))) (S (K K) I)))) I))) (S (K K) I))))) I))) (S (K K) (S (K (S (K (S I (K (S (K K) I)))) (S (K (S I (K (K I)))) I))) I)))) I))))) (S (K (S (S (K (S (K (S (S (K ((S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (K (S (K (S (K (S I I)) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S I I)))))) (K (K I))))))) (S (K (S (S (K S) (S (K K) (S (K S) (S (K (S (S (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) (S (K (S (K (S I (K (S (K K) I)))) I)) I)))) (S (K K) I))))))) (S (K K) (S (S (K S) (S (K K) (S (K S) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I (K (S (K K) I)))) (S (K (S I (K (K I)))) I))) I)))))) (K (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I (K (K I)))) (S (K (S I (K (K I)))) I))) I))))))))))) (K (K I))) (S (K (S (K ((S (S (K S) (S (K K) (S (K S) (S (K (S I)) (S (K K) I))))) (K (S (K K) I))) (K I))))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K K) (S (K S) (S (K (S I)) (S (K K) I))))) (K (S (K K) I)))) I))) (K I))))) I))) (S (K K) I))) (S (S (K (S (S (K S) (S (K K) (S (K (S (K (S I I)) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S I I)))))) (K (K I))))) (S (K (S (K (S (S (S (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) (S (K (S (K (S I (K (S (K K) I)))) I)) I)) (K (((S (S (K S) (S (K K) (S (K S) (S (K (S I)) (S (K K) I))))) (K (S (K K) I))) (S (K K) I)) (S (K K) I)))))))) (S (S (K S) (S (K (S (K S))) (S (S (K S) (S (K K) (S (K S) (S (K (S (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))))) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I (K (S (K K) I)))) (S (K (S I (K (K I)))) I))) I))))))) (K (S (K (S (S (K (S (K (S (K ((S (S (K S) (S (K K) (S (K S) (S (K (S I)) (S (K K) I))))) (K (S (K K) I))) (K I))))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K K) (S (K S) (S (K (S I)) (S (K K) I))))) (K (S (K K) I)))) I))) (K I)))) (S (K (S (K (S I (K (S (K K) I)))) (S (K (S I (K (K I)))) I))) I)))) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I (K (K I)))) (S (K (S I (K (K I)))) I))) I)))))))) (K (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I (K (K I)))) (S (K (S I (K (K I)))) I))) I))))))))) (K I))) (S (K (S (S (K (S (S (K S) (S (K (S (K (S (S (K S) (S (S (K S) (S (K K) I)) (K I))) (S (K K) I))))) (S (S (K S) (S (K K) (S (K (S (K (S (K (S (S I (K (K (K I)))) (K (S (K K) I)))))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K S))) (S (K (S (K (S (K S))))) (S (K (S (K (S (K K))))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (K (S (S I (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K S))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I)))) (S (K (S (K K))) (S (K (S I)) (S (K K) I))))))))) (K (K (S (K K) I)))))) (K (K (K I))))) I))) (K I))))) (K (K I))))))) (S (K K) I))))) (K (K I))))))) (K (K (K I))))) I))) (K I)))) I))) (K I)))) (S (K (S (S (K (S (K (S (K (S (S I (K (K (K I)))) (K (S (K K) I)))))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K S))) (S (K (S (K (S (K S))))) (S (K (S (K (S (K K))))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (K (S (S I (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K S))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I)))) (S (K (S (K K))) (S (K (S I)) (S (K K) I))))))))) (K (K (S (K K) I)))))) (K (K (K I))))) I))) (K I))))) (K (K I))))))) (S (K K) I))))) (K (K I))))))) (K (K (K I))))) I))) (K I)))) I))) (S (K K) I)))) I))) (S (K K) (S (K (S (K (S I (K (S (K K) I)))) (S (K (S I (K (K I)))) I))) I)))) I)))) (S (S (K S) (S (K K) I)) (K (S (S (K (S (S (K S) (S (K K) (S (K (S (K (S I I)) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S I I)))))) (K (K I))))) (S (K (S (K (S (S (S (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) (S (K (S (K (S I (K (S (K K) I)))) I)) I)) (K (((S (S (K S) (S (K K) (S (K S) (S (K (S I)) (S (K K) I))))) (K (S (K K) I))) (S (K K) I)) (S (K K) I)))))))) (S (S (K S) (S (K (S (K S))) (S (S (K S) (S (K K) (S (K S) (S (K (S (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))))) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I (K (S (K K) I)))) (S (K (S I (K (K I)))) I))) I))))))) (K (S (K (S (S (K (S (K (S (K ((S (S (K S) (S (K K) (S (K S) (S (K (S I)) (S (K K) I))))) (K (S (K K) I))) (K I))))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K K) (S (K S) (S (K (S I)) (S (K K) I))))) (K (S (K K) I)))) I))) (K I)))) (S (K (S (K (S I (K (S (K K) I)))) (S (K (S I (K (K I)))) I))) I)))) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I (K (K I)))) (S (K (S I (K (K I)))) I))) I)))))))) (K (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I (K (K I)))) (S (K (S I (K (K I)))) I))) I))))))))) (K I))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K (S (S (K S) (S (S (K S) (S (K K) I)) (K I))) (S (K K) I))))) (S (S (K S) (S (K K) (S (K (S (K (S (K (S (S I (K (K (K I)))) (K (S (K K) I)))))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K S))) (S (K (S (K (S (K S))))) (S (K (S (K (S (K K))))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (K (S (S I (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K S))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I)))) (S (K (S (K K))) (S (K (S I)) (S (K K) I))))))))) (K (K (S (K K) I)))))) (K (K (K I))))) I))) (K I))))) (K (K I))))))) (S (K K) I))))) (K (K I))))))) (K (K (K I))))) I))) (K I)))) I))) (K I)))) (S (K (S (K (S (S I (K (K I))) (K (S (K K) I)))))) (S (K (S (S (K (S (S (K S) (S (K (S (K (S (S (K S) (S (S (K S) (S (K K) I)) (K I))) (S (K K) I))))) (S (S (K S) (S (K K) (S (K (S (K (S (K (S (S I (K (K (K I)))) (K (S (K K) I)))))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K S))) (S (K (S (K (S (K S))))) (S (K (S (K (S (K K))))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (K (S (S I (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K S))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I)))) (S (K (S (K K))) (S (K (S I)) (S (K K) I))))))))) (K (K (S (K K) I)))))) (K (K (K I))))) I))) (K I))))) (K (K I))))))) (S (K K) I))))) (K (K I))))))) (K (K (K I))))) I))) (K I)))) I))) (K I)))) (S (K (S (S (K (S (K (S (K (S (S I (K (K (K I)))) (K (S (K K) I)))))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K S))) (S (K (S (K (S (K S))))) (S (K (S (K (S (K K))))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (K (S (S I (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K S))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I)))) (S (K (S (K K))) (S (K (S I)) (S (K K) I))))))))) (K (K (S (K K) I)))))) (K (K (K I))))) I))) (K I))))) (K (K I))))))) (S (K K) I))))) (K (K I))))))) (K (K (K I))))) I))) (K I)))) I))) (S (K K) I)))) I))) (S (K K) I))))) (S (K (S (K (S I (K (S (K K) I)))) (S (K (S I (K (K I)))) I))) I)))) (K I))) I)))))))<\/span>
\n<\/details>\n

and<\/p>\n

\nSieve of\u00a0Eratosthenes in X<\/strong> calculus<\/summary>\n


\n(((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) ((X (X (X (X X)))) (X X) (X X))))))) ((X (X (X X))) ((X (X (X X))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) (X X))) (X X))) ((X (X (X X))) ((((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))) ((X (X (X X))) (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) (X X)))) ((X (X (X X))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) ((X (X (X (X X)))) (X X) (X X))))))) ((X (X (X X))) ((X (X (X X))) (X X)))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) (X X))) (X X))) ((X (X (X X))) ((((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) (X X)))) (X X)))))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))) ((X (X (X X))) (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) (X X)))) ((X (X (X X))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) (X X)))) (X X))))))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) (X X)))) (X X)))))))))) ((X (X (X X))) (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X)))))) (X X)))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X)))))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X)))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X)))))) (X X)))) ((X (X (X X))) (X X))))) (X X)))) ((X (X (X X))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X)))))) (X X)))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X)))))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X)))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X)))))) (X X)))) ((X (X (X X))) (X X))))) (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))) ((X (X (X X))) (X X)))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) ((X (X (X (X X)))) (X X) (X X))))))) ((X (X (X X))) ((X (X (X X))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X)))))) (X X)))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X)))))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X)))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X)))))) (X X)))) ((X (X (X X))) (X X))))) (X X)))) ((X (X (X X))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X)))))) (X X)))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X)))))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X)))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X)))))) (X X)))) ((X (X (X X))) (X X))))) (X X)))) ((X (X (X X))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X)))))) (X X)))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X)))))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X)))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X)))))) (X X)))) ((X (X (X X))) (X X))))) (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) (X X)))) (X X)))) (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))) ((X (X (X X))) (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) (X X)))) ((X (X (X X))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X)))))) (X X)))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X)))))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X)))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X)))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) (X X)))) (X X)))) (X X)))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))) ((X (X (X X))) (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) (X X)))) ((X (X (X X))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) (X X)))) (X X)))) (X X))) ((X (X (X X))) ((((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))))))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))) ((X (X (X X))) (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) (X X)))) ((X (X (X X))) (X X))))) (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))) ((X (X (X X))) (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) (X X)))) ((X (X (X X))) (X X))))) (X X)) ((X (X (X X))) ((((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))))))) (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X X))) (X X))))) (X X)))) (X X))))))) (X X)))))))
\n<\/span>
\n<\/details>\n

The focus of this post is to introduce\u00a0a tool (written in Clojure) that lets you play with SKI<\/strong> and X<\/strong> encodings. The inspiration for me to write this entry was this post \u03bb-\u0438\u0441\u0447\u0438\u0441\u043b\u0435\u043d\u0438\u0435 \u0438 LISP<\/a> (in Russian), which showed how to encode Boolean logic, Church numerals and arithmetic operations on them, Y<\/strong> combinator and a few very common functions such as map<\/em>, reduce<\/em> and filter<\/em> in pure lambda calculus. The translator then can translate all these functions and the functions that use them\u00a0into\u00a0SKI<\/strong>\u00a0and\u00a0X<\/strong>\u00a0 expressions.<\/p>\n

The main challenges to overcome were dealing with the variable arity of lambda functions, which is not straightforward\u00a0to deal with in Clojure, and more importantly making Clojure “lazier” to make sure that we can implement Y<\/strong>\u00a0combinator and the functions that are using it. It was also interesting to implement a lesser known variant \u00a0of Y<\/strong> combinator for mutually recursive functions, called Y*<\/strong> and obtain its translation. Finally, it was interesting to implement map<\/em> and filter<\/em> by just using reduce<\/em> (fold<\/em>) functions. While not terribly surprising, it means that we only need Y<\/strong> combinator for fold<\/em> – map<\/em> and filter<\/em> can use Y<\/strong> indirectly by relying on fold<\/em> in their implementation.<\/p>\n

Why do we need our own numbers, arithmetic and logic operations? We cannot use any build-in numbers or arithmetic operators because we want everything to be expressed using just combinators. One of the possibilities is to use Church encoding<\/a>, which is what we are using\u00a0in this post.\u00a0For example, \u00a0the expression 7*7-7 has this representation in SKI<\/strong>:
\n(((S (S (K S) (S (K (S (K S))) (S (K (S (K (S (K S))))) (S (K (S (K (S (K K))))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (K (S (S I (K (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) (S (K (S (S (K S) (S (K (S (K S))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S (K (S (K (S I)))) (S (K (S (K K))) (S (K (S I)) (S (K K) I))))))))) (K (K (S (K K) I)))))) (K (K (K I))))) I))) (K I))))) (K (K I))))))) (S (K K) I))))) (K (K I))))))) (K (K (K I)))) (((S (S (K S) (S (K (S (K S))) (S (K (S (K (S (K S))))) (S (K (S (K (S (K K))))) (S (S (K S) (S (K K) (S (K S) (S (K K) I)))) (K (S (S (K S) (S (K K) I)) (K I)))))))) (K (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) (K I))))))))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) (K I)))))))))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) ((S (K (S (S (K S) (S (K K) I)))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K I))))) (K (K I)))) (K I)))))))))<\/span><\/p>\n

The\u00a0X<\/strong>\u00a0version\u00a0of the same is lengthier:\u00a0<\/p>\n

\n42 in X<\/strong><\/summary>\n


\n((((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) (X X) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X)))))) (X X)))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X)))))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X)))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X))))) ((((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X))))))))) ((X (X (X X))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) ((X (X (X X))) (X X)))))))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) ((X (X (X X))) (X X))))))))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) (((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))))) ((X (X (X (X X)))) ((X (X (X X))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))))) ((X (X (X (X X)))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X (X X))))) ((X (X (X (X X)))) ((X (X (X X))) (X (X (X X)))) (X X))) ((X (X (X X))) (X X)))))) ((X (X (X X))) ((X (X (X X))) (X X))))) ((X (X (X X))) (X X))))))))))<\/span>
\n<\/details>\n

\u00a0As you can see the representations are very verbose, partly by the nature of encodings, partly by the fact that no optimizations were done in the translator. The code above is actually a valid Clojure code, and can be executed. Below I describe the necessary scaffolding to make that happen.<\/p>\n

Project layout<\/h3>\n

This is a leiningen<\/a> project consisting of four source files and a couple of test files. The source files are listed below in order of\u00a0dependencies\u00a0between them.<\/p>\n

    \n
  1. combinator_definitions.clj<\/em> – contains definitions of all combinators and supporting functions.<\/li>\n
  2. lambda_to_ski_translator.clj<\/em> – this file contains the source code for the translator.<\/li>\n
  3. ski_encoding.clj<\/em> – contains definitions of functions and their translations to SKI<\/strong> calculus.<\/li>\n
  4. iota_encoding.clj<\/em> – contains code to translate from SKI<\/strong> calculus to X<\/strong>\u00a0and also contains a few examples.<\/li>\n<\/ol>\n

    Executing iota_encoding.clj<\/em> will pull dependencies and execute the code from all other source files. The code was developed in LightTable<\/a>.<\/p>\n

    I wanted to write\u00a0a simple self-contained system, which is easy to understand and modify, so translations produced are far from optimal, but the code is quite compact and follows from the first principles. There are other related\u00a0projects, notably, unlambda<\/a>, LazyK<\/a>, and pointfree<\/a> package of Haskell (used by the LamdaBot<\/a>).<\/p>\n

    Working with Variadic Functions<\/h3>\n

    First, we need to get around the fact that a function application in Clojure would throw an ArityException<\/em> if we don’t supply the exact number of arguments that the function expects:<\/p>\n

    \r\n(defn fun1 [x] x)\r\n(fun1) ; throws ArityException - too few parameters\r\n(fun1 fun1 fun1) ; throws ArityException - too many parameters\r\n<\/pre>\n
    In contrast,\u00a0\u03bbx.x<\/strong><\/em> and (\u03bbx.x) (\u03bby.y) (\u03bbz.z)<\/strong><\/em>\u00a0are both well-formed lambda expressions and evaluate to \u03bbx.x<\/strong><\/em> and \u03bbz.z<\/strong><\/em> respectively. The first expression expects one argument, but gets none, while in the second expression,\u00a0(\u03bbx.x)\u00a0<\/strong><\/em>expects one argument but gets two –\u00a0(\u03bby.y)<\/strong><\/em> and\u00a0(\u03bbz.z)<\/strong><\/em>\u00a0(so it consumes the first one, returns a function, which, in turn, consumes the the second argument, returning another function).<\/p>\n
    To resolve this difficulty we will use variadize<\/em>\u00a0function defined in combinator_definitions.clj<\/em>. Below is given the strict variant of this function – it works well for arithmetics and boolean logic but is not “lazy enough” to work for\u00a0Y<\/strong> and Y*<\/strong> combinators. Modifications to cover these fixed-point combinators are given below.<\/p>\n
    \r\n(defn variadize-strict\r\n  ([fnct] (variadize-strict fnct (arg-count fnct)))\r\n  ([fnct num-args]\r\n   (if (zero?  num-args) (fnct)\r\n       (fn [& args]\r\n         (cond\r\n           (> (count args) num-args) (apply (apply fnct (take num-args args)) (drop num-args args))\r\n           (= (count args) num-args) (apply fnct args)\r\n           :else (variadize-strict (reduce partial fnct args) (- num-args (count args))))))))<\/pre>\n
    The function takes the function to be “variadized” and the number of arguments it expects. If that number is not provided, it’s determined using Java reflection by arg-count<\/em> function. The function returned by variadize-strict<\/em> keeps track of the argument it had been supplied with at the moment of the call. If this number is less than the expected number, we use partial application (curring), it it’s exactly the expected number then we simply apply the variadized-strict<\/em>\u00a0to the arguments, and if there more arguments than the function is expecting, then we apply the function to the number of arguments it expects and the remaining arguments are supplied to the result of the that application. Please see unit-tests in combinator_definitions_test.clj<\/em> \u00a0for examples.<\/p>\n
    Since we have only four basic combinators that we are working with – S<\/strong>, K<\/strong>, I<\/strong>, and X<\/strong>, it’s straightforward to variadize all of them. For instance, here is how we are defining\u00a0S<\/strong>:<\/p>\n
    \r\n(defn S-def [f g x] (f x (g x))) (def S (variadize S-def))\r\n<\/pre>\n
    Note that implementation of the same functionality just by using multi-arity and variadic functions in Clojure is not straightforward, and will likely to result in more convoluted code.<\/p>\n
    A note on SKI combinatorial calculus<\/h3>\n
    Here are definitions of S<\/strong>, K<\/strong>, and I<\/strong> (see SKI combinator calculus<\/a>):<\/p>\n