Combinatory logic

From HaskellWiki

General[edit]

Although combinatory logic has precursors, it was Moses Schönfinkel who first explored combinatory logic as such. Later the work was continued by Haskell B. Curry. Combinatory logic was developed as a theory for the foundation of mathematics [Bun:NatICL], and it has relevance in linguistics too.

Its goal was to understand paradoxes better, and to establish fundamental mathematical concepts on simpler and cleaner principles than the existing mathematical frameworks, especially to understand better the concept of substitution. Its “lack of (bound) variables” relates combinatory logic to the pointfree style of programming. (For contrast, see a very different approach which also enables full elimination of variables: recursive function theory)

General materials:

Portals and other large-scale resources[edit]

Applications[edit]

Of course combinatory logic has significance in the foundations of mathematics, or in functional programming, computer science. For example, see Chaitin's construction.

It is interesting that it can be important also in some linguistical theories. See especially the theory of applicative universal grammar, it uses many important thoughts from combinatory logic.

Lojban is an artificial language (and, unlike the more a posteriori Esperanto, it is rather of an a priori taste). It is a human language, capable of expressing everything. Its grammar uses (among others) things taken from mathematical logic, e.g. predicate-like structures. Although its does not make use combinatory logic directly (even, from a category logic / functional programming point of view, it uses also rather imperative ideas), but it may give hints and analogies, how combinatry logic can be useful in linguistics.

Implementing CL[edit]

  • Talks about it at haskell-cafe Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \subset} haskell-cafe
  • Lot of interpreters at John's Lambda Calculus and Combinatory Logic Playground.
  • Unlambda resources concerning David Madore's combinatory logic programming language Unlambda
  • CL++, a lazy-evaluating combinatory logic interpreter with some computer algebra service: e.g. it can reply the question Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf+\;\mathbf2\;\mathbf3;} with Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf5} instead of a huge amount of parantheses and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf K} , Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf S} combinators. Unfortunately I have not written it directly in English, so all documentations, source code and libraries are in Hungarian. I want to rewrite it using more advanced Haskell programming concepts (e.g. monads or attribute grammars) and directly in English.

Base[edit]

Some thoughts on base combinators and on the relatedness of their rules to other topics

  • Conal Elliott's reply to thread zips and maps
  • Intuitionistic fragment of propositional logic
  • Records in function: in set theory and database theory, we regard functions as consisting of more elementary parts, records: a function Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f} can be regarded as the set of all its records. A record is a pair of a key and its value, and for functions we expect unicity (and sometimes stress this requirement by writing Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x \mapsto x'} instead of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \left\langle x,\;y\right\rangle} ).Sometimes I think of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf S} as having a taste of record selection: Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf S\;c\;f\;x} selects a record determinated by key Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} in function Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f} (as in a database), and returns the found record (i.e. corresponding key and value) contained in the Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle c} container (continuation). Is this thought just a toy or can it be brought further? Does it explain why Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf S} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf K} can constitute a base?
  • Also bracket abstraction gives us a natural way to understand the seemingly rather unintuitive and artificial Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf S} combinator better

Programming in CL[edit]

I think many thoughts from John Hughes' Why Functional Programming Matters can be applied to programming in Combinatory Logic. And almost all concepts used in the Haskell world (catamorphisms etc.) help us a lot here too. Combinatory logic is a powerful and concise programming language. I wonder how functional logic programming could be done by using the concepts of Illative combinatory logic, too.

Datatypes[edit]

Continuation passing for polynomial datatypes[edit]

Direct product[edit]

Let us begin with a notion of the ordered pair and denote it by Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Diamond_2} . We know this construct well when defining operations for booleans

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{true} \equiv \mathbf K}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{false} \equiv \mathbf{K_*}}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{not} \equiv \mathbf{\Diamond_2}\;\mathbf{false}\;\mathbf{true}}

and Church numbers. I think, in generally, when defining datatypes in a continuation-passing way (e.g. Maybe or direct sum), then operations on so-defined datatypes often turn to be well-definable by some Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{\Diamond_n}} .

We define it with

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{\Diamond_2} \equiv \lambda\;x\;y\;f\;.\;f\;x\;y}

in Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \lambda} -calculus and

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{\Diamond_2} \equiv\;\mathbf{C_{(1)}}\;\mathbf{C_*}}

in combinatory logic.

A nice generalization scheme:

  • as the Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \langle\dots\rangle} construct can be generalized to any natural number Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle n} (the concept of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle n} -tuple, see Barendregt's Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \lambda} Calculus)
  • and in this generalized scheme Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf I} corresponds to the 0 case, Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{C_*}} to the 1 case, and the ordered pair construct Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Diamond_2} to the 2 case, as though defining
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{\Diamond_0} \equiv \mathbf I}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{\Diamond_1} \equiv \mathbf{C_*}}

so we can write definition

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{\Diamond_2} \equiv \mathbf{C_{(1)}}\;\mathbf{C_*}}

or the same

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{\Diamond_2} \equiv \mathbf C \cdot \mathbf{C_*}}

in a more interesting way:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{\Diamond_2} \equiv \mathbf C\cdot\mathbf{\Diamond_1}}

Is this generalizable? I do not know. I know an analogy in the case of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{left}} , Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{right}} , Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{just}} , Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{nothing}} .

Direct sum[edit]

The notion of ordered pair mentioned above really enables us to deal with direct products. What about it dual concept? How to make direct sums in Combinatory Logic? And after we have implemented it, how can we see that it is really a dual concept of direct product?

A nice argument described in David Madore's Unlambda page gives us a continuation-passig style like solution. We expect reductions like

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{left}\;x \to \lambda\;f\;g\;.\;f\;x}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{right}\;x \to \lambda\;f\;g\;.\;g\;x}

so we define

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{left} \equiv \lambda\;x\;f\;g\;.\;f\;x}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{right} \equiv \lambda\;x\;f\;g\;.\;g\;x}

now we translate it from Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \lambda} -calculus into combinatory logic:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{left} \equiv \mathbf{K_{(2)}}\;\mathbf{C_*}}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{right} \equiv \mathbf{K_{(1)}}\;\mathbf{C_*}}

Of course, we can recognize Haskell's direct sum construct 

 Either (Left, Right)

implemented in an analogous way.

Maybe[edit]

Let us remember Haskell's maybe: 

 maybe :: a' -> (a -> a') -> Maybe a -> a'
 maybe n j Nothing = n
 maybe n j (Just x) = j x

thinking of

  • n as nothing-continuation
  • j as just-continuation

In a continuation passing style approach, if we want to implement something like the Maybe constuct in Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \lambda} -calculus, then we may expect the following reductions:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{nothing} \equiv \lambda\;n\;j\;.\;n}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{just}\;x\;\to\;\lambda\;n\;j\;.\;j\;x}

we know both of them well, one is just Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf K} , and we remember the other too from the direct sum:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{nothing} \equiv \mathbf K}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{just} \equiv \mathbf{right}}

thus their definition is

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{nothing} \equiv \mathbf K}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{just} \equiv \mathbf{K_{(1)}}\;\mathbf{C_*}}

where both Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{just}} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{right}} have a common definition.

Maybe2[edit]

Haskell: 

 module Maybe2 (Maybe2, maybe2, nothing2, just2) where

 data Maybe2 a b = Nothing2 | Just2 a b

 maybe2 :: maybe2ab' -> (a -> b -> maybe2ab') -> Maybe2 a b -> maybe2ab'
 maybe2 nothing2Cont _ Nothing2 = nothing2Cont
 maybe2 _ just2Cont (Just2 a b) = just2Cont a b

 nothing2 :: Maybe2 a b
 nothing2 = Nothing2

 just2 :: a -> b -> Maybe2 a b
 just2 = Just2

Expected reductions:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{nothing2}\;n\;j \ge n}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{just2}\;a\;b\;n\;j \ge j\;a\;b}

Other argument orders are possible, too, but they lead to more complicated solutions than the following:

Combinators:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{nothing2} \equiv \mathbf K}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{just2} \equiv \mathbf{K_{\left(2\right)}} \mathbf{\Diamond_2}}


Conjecture for generalisation:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{nothing_n} \equiv \mathbf K}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{just_n} \equiv \mathbf{K_{\left(n\right)}} \mathbf{\Diamond_n}}

with straightforward generalisations, e.g.

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{\Diamond_1} \equiv \mathbf{C_*}}

Catamorphisms for recursive datatypes[edit]

List[edit]

Let us define the concept of list by its catamorphism (see Haskell's foldrfunction): a list (each concrete list) is a function taking two arguments

  • a two-parameter function argument (cons-continuation)
  • a zero-parameter function argument (nil-continuation)

and returns a value coming from a term consisting of applying cons-continuations and nil-continuations in the same shape as the correspondig list. E. g. in case of having defined

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{oneTwoThree} \equiv \mathbf{cons}\;\mathbf1\;\left( \mathbf{cons}\;\mathbf2\;\left(\mathbf{cons}\;\mathbf3\;\mathbf{nil}\right) \right)}

the expression

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{oneTwoThree}\;\mathbf+\;\mathbf0}

reduces to

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf+\;\mathbf1\;\left(\mathbf+\;\mathbf2\; \left(\mathbf+\;\mathbf3\;\mathbf0\right)\right)}

But how to define Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{cons}} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{nil}} ? In Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \lambda} -calculus, we should like to see the following reductions:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{nil}\;c\;n\;\to\;\;n}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{cons}\;h\;t\; \to \;\lambda\;c\;n\;.\;c\;h\;\left(t\;c\;n\right)}

Let us think of the variables as Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle h} denoting head, Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t} denoting tail, Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle c} denoting cons-continuation, and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle n} denoting nil-continuation.

Thus, we could achieve this goal with the following definitions:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{nil} \equiv \lambda\;c\;n\;.\;n}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{cons} \equiv \lambda\;h\;t\;c\;n\;.\;c\;h\;\left(t\;c\;n\right)}

Using the formulating combinators described in Haskell B. Curry's Combinatory Logic I, we can translate these definitions into combinatory logic without any pain:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{nil} \equiv \mathbf K_*}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{cons} \equiv \mathbf B \left( \mathbf{\Phi}\;\mathbf B \right) \mathbf{C_*}}

Of course we could use the two parameters in the opposite order, but I am not sure yet that it would provide a more easy way.

A little practice: let us define concat. In Haskell, we can do that by 

 concat = foldr (++) []

which corresponds in cominatory logic to reducing

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{concat}\;l\equiv l\;\mathbf{append}\;\mathbf{nil}}

Let us use the ordered pair (direct product) construct:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{concat}\equiv \mathbf{\Diamond_2}\;\mathbf{append}\;\mathbf{nil}}

and if I use that nasty Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{centred}} (see later)

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{concat} \equiv \mathbf{centred}\;\mathbf{append}}

Monads in Combinatory Logic?[edit]

Concrete monads[edit]

Maybe as a monad[edit]
return[edit]

Implementing the return monadic method for the Maybe monad is rather straightforward, both in Haskell and CL: 

 instance Monad Maybe
         return = Just
         ...

in Haskell and

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{maybe\!\!-\!\!return} \equiv \mathbf{just}}

in combinatory logic.

map[edit]

Haskell: 

 instance Functor Maybe where
         map f = maybe Nothing (Just . f)

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \lambda} -calculus: Expected reductions:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{maybe\!\!-\!\!map}\;f\;p\;\to\;p\;\mathbf{nothing}\;\left(\mathbf{just_{(1)}}\;f\right)}

Definition:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{maybe\!\!-\!\!map}\equiv \lambda\;f\;p\;.\;p\;\mathbf{nothing}\;\left(\mathbf{just_{(1)}}\;f\right)}

Combinatory logic: we expect the same reduction here too

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{maybe\!\!-\!\!map}\;f\;p\;\to\;p\;\mathbf{nothing}\;\left(\mathbf{just_{(1)}}\;f\right)}

let us get rid of one parameter:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{maybe\!\!-\!\!map}\;f\;\to\;\mathbf{\Diamond_2}\;\mathbf{nothing}\;\left(\mathbf{just_{(1)}}\;f\right)}

now we have the definition:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{maybe\!\!-\!\!map}\equiv \mathbf{\Diamond_2}\;\mathbf{nothing}\;\cdot\;\mathbf{just_{(1)}}}
bind[edit]

Haskell: 

 instance Monad Maybe (>>=) where
         (>>=) f p = maybe Nothing f

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \lambda} -calculus: we expect

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{maybe\!\!-\!\!=\!\!<\!\!<}\;f\;p\;\to\;p\;\mathbf{nothing}\;f}

achieved by defintion

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{maybe\!\!-\!\!=\!\!<\!\!<} \equiv \lambda\;f\;p\;.\;p\;\mathbf{nothing}\;f}

In combinatory logic the above expected reduction

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{maybe\!\!-\!\!=\!\!<\!\!<}\;f\;p\;\to\;p\;\mathbf{nothing}\;f}

getting rid of the outest parameter

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{maybe\!\!-\!\!=\!\!<\!\!<}\;f\;\to\;\mathbf{\Diamond_2}\;\mathbf{nothing}\;f}

yielding definition

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{maybe\!\!-\!\!=\!\!<\!\!<} \equiv \mathbf{\Diamond_2}\;\mathbf{nothing}}

and of course

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{maybe\!\!-\!\!\!>\!\!>\!\!=} \equiv \mathbf C\;\mathbf{maybe\!\!-\!\!=\!\!<\!\!<}}

But the other way (starting with a better chosen parameter order) is much better:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{maybe\!\!-\!\!\!>\!\!>\!\!=}\;p\;f\;\to\;p\;\mathbf{nothing}\;f}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{maybe\!\!-\!\!\!>\!\!>\!\!=}\;p\;\to\;p\;\mathbf{nothing}}

yielding the much simplier and more efficient definition:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{maybe\!\!-\!\!\!>\!\!>\!\!=} \equiv \mathbf{C_*}\;\mathbf{nothing}}

We know already that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{C_*}} can be seen as as a member of the scheme of tuples: Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{\Diamond_n}} for Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle n=1} case. As the tupe construction is a usual guest at things like this (we shall meet it at list and other maybe-operations like Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{maybe\!\!-\!\!join}} ), so us express the above definition with Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{C_*}} denoted as Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Diamond_1} :

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{maybe\!\!-\!\!\!>\!\!>\!\!=} \equiv \mathbf{\Diamond_1}\;\mathbf{nothing}}

hoping that this will enable us some interesting generalization in the future.

But why we have not made a more brave generalization, and express monadic bind from monadic join and map? Later in the list monad, we shall see that it may be better to avoid this for sake of deforestation. Here a maybe similar problem will appear: the problem of superfluous Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf I} .

join[edit]
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{maybe\!\!-\!\!join} \equiv \mathbf{\Diamond_2}\;\mathbf{nothing}\;\mathbf I}

We should think of changing the architecture if we suspect that we could avoid Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf I} and solve the problem with a more simple construct.


The list as a monad[edit]

Let us think of our list-operations as implementing monadic methods of the list monad. We can express this by definitions too, e.g.

we could name

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{list\!\!-\!\!join} \equiv \mathbf{concat} }

Now let us see mapping a list, concatenating a list, binding a list. Mapping and binding have a common property: yielding nil for nil. I shall say these operations are centred: their definition would contain a Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf C\;\mathbf{\Diamond_2}\;\mathbf{nil}} subexpression. Thus I shall give a name to this subexpression:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{centred} \equiv \mathbf C\;\mathbf{\Diamond_2}\;\mathbf{nil}}

Now let us define map and bind for lists:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{list\!\!-\!\!map} \equiv \mathbf{centred}_{(1)}\;\mathbf{cons}_{(1)}}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{list\!\!-\!\!=\!\!<\!\!<} \equiv \mathbf{centred}_{(1)}\;\mathbf{append}_{(1)}}

now we see it was worth of defining a common Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{centred}} . But to tell the truth, it may be a trap. Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{centred}} breaks a symmetry: we should always define the cons and nil part of the foldr construct on the same level, always together. Modularization should be pointed towards this direction, and not to run forward into the T-street of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{centred}} .

Another remark: of course we can get the monadic bind for lists

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{list\!\!-\!\!\!>\!\!>\!\!=} \equiv \mathbf{C}\;\mathbf{list\!\!-\!\!=\!\!<\!\!<}}

But we used Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{append}} here. How do we define it? It is surprisingly simple. Let us think how we would define it in Haskell by foldr function, if it was not defined already as ++ defined in Prelude: In defining 

 (++) list1 list2

we can do it by foldr: 

 (++) [] list2 = list2
 (++) (a : as) list2 = a : (++) as list2

thus 

 (++) list1 list2 = foldr (:) list2 list1

let us se how we should reduce its corresponding expression in Combinatory Logic:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{append}\;l\;m \to l\;\mathbf{cons}\;m}

thus

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{append}\,l\,m = l\,\mathbf{cons}\,m}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{append}\;l =\!\!_1\;l\;\mathbf{cons}}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{append} \equiv \mathbf{C_*}\;\mathbf{cons} }

Thus, we have defined monadic bind for lists. I shall call this the deforested bind for lists. Of course, we could define it another way too: by concat and map, which corresponds to defining monadic bind from monadic map and monadic join. But I think this way forces my CL-interpreter to manage temporary lists, so I gave rather the deforested definition.

Defining the other monadic operation: return for lists is easy: 

 instance Monad [] where
         return = (: [])

in Haskell -- we know, 

 (: [])

translates to 

 return = flip (:) []

so we can see how to do it in combinatory logic:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{list\!\!-\!\!return} \equiv \mathbf C\;\mathbf{cons}\;\mathbf{nil}}

How to AOP with monads in Combinatory Logic?[edit]

We have defined monadic list in CL. Of course we can make monadic Maybe, binary tree, Error monad with direct sum constructs...

But separation of concerns by monads is more than having a bunch of special monads. It requires other possibilities too: e.g. being able to use monads generally, which can become any concrete mondads.

Of course my simple CL interpreter does not know anything on type classes, overloading. But there is a rather restricted andstatic possibility provided by the concept of definition itself:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{work} \equiv \mathbf{A\!\!-\!\!\!>\!\!>\!\!>\!\!=}\;\mathbf{subwork\!\!-\!\!1}\;\mathbf{parametrized\!\!-\!\!subwork\!\!-\!\!2}}

and later we can change the binding mode named A e.g. from a failure-handling Maybe-like one to a more general indeterminism-handling list-like one, then we can do that simply by replacing definition

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{A\!\!\!-\!\!>\!\!>\!\!>\!\!=} \equiv \mathbf{maybe\!\!\!-\!\!>\!\!>\!\!>\!\!=}}

with definition

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{A\!\!\!-\!\!>\!\!>\!\!>\!\!=} \equiv \mathbf{list\!\!\!-\!\!>\!\!>\!\!>\!\!=} }

Self-replication, quines, reflective programming[edit]

Background[edit]

David Madore's Quines (self-replicating programs) and Shin-Cheng Mu's many writings, including a Haskell quine give us wonderful insights on mathematical logic, programming, self-reference. Wikipedia's quine page and John Bethencourt's quine quine. See also the writings of Raymond Smullyan, Hofstadter, also his current research project on a self-watching cognitive architecture, Manfred Eigen and Ruthild Winkler: Laws of the Game / How the Principles of Nature Govern Chance, and Karl Sigmund's Games of Life, and Reflective programming (see Reflection '96 and P. Maes & D. Nardi: Meta-Level Architectures and Reflection). G.J. Chaitin especially his Understandable Papers on Incompleteness, especially The Unknowable (the book is available on this page, just roll the page bellow that big colored photos). The book begins with the limits of mathematics: Gödel's undecidable, Turing's uncompatiblity, Chaitin's randomness); but (or exactly that's why?) it ends with writing on the future and beuty of science.

I must read Autopoesis and The Tree of Knowledge carefully from Maturana and Varela to say if their topics are releted to here. See

Self-replication[edit]

Quines: the idea of self-replication can be conveyed by the concept of a program, which is able to print its own list. But pure Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \lambda} -calculus and combinatory logic does not know any notion of printing! We should like the capture the essence of self-replication, without resorting to the imperative world.

Representation, qoutation -- the DNA[edit]

Let us introduce the concept of representing combinatory logic terms. How could we do that? For example, by binary trees. The leaves should represent the base combinators, and the branches mean application.

And how to represent combintory logic terms -- in combinatory logic itself? The first thought could be, that it is not a problem. Each combinatory logic term could be represented by itself.

Sometimes this idea works. The huge power of higher order functions is exactly in being able to treat datas programs and vice versa. Sometimes we are enabled to do things, which could be done in other languages only by carefully designing a representation, a specific language.

But sometimes, representing CL terms by themselves is not enough. Let us imagine a tutoring program! Let the topic be combinatory logic, the language of implementation -- combinatory logic, too. How should the tutoring program ask the pupil questions like:

Tell me if the following two expresions have the same normal form:
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf K\;\mathbf{24}\;\mathbf{48}}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{24}}

The problem is that our program is simply unable to distinguish between CL terms which have the same normal form (in fact, equivalence cannot be defined generally either). If we represent CL terms by themselves, we simply loose a lot of information, including loosing any possibility to make distinctions between equivalent terms.

We see that there is something that relates to make a distinction between target language and metalanguage (See Imre Ruzsa, or Haskell B. Curry)

In this example, the distinction is:

  • We deal with combinatory logic expressions because our program has to teach them: it is related to it just like a vocabulary program is related to English.
  • But we deal with programming logic expressions because our program is implemented in them. Just like VIM is related to C++.

We said CL terms are eventually trees. Let us represent them with trees then -- now let us think of trees not as of term trees, but as datatypes which we must construct by hand, in a similar way as we defined Maybes, direct sums, direct products, lists.

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf K}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{leaf}\;\mathbf{true}}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf S}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{leaf}\;\mathbf{false}}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \left(a\;b\right)}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{branch}\;\alpha\;\beta}

where let Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \alpha} denote the representation of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle a} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \beta} that of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle b}

Let us make a distinction between term trees and datatype trees. A Haskell example:

  • many Haskell expressions can be regarded as term trees
  • but only special Haskell expressions can be seen as datatype trees: those who are constructed from Branch and Leaf in an appropriate way

Similarly,

  • all CL expressions can be regarded as term trees.
  • but CL expressions which can be revered as datatype trees must obey a huge amount of constraints: they may consist only of subexpressions Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{leaf}} , Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{branch}} , Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{true}} , Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{false}} subexpressions in an approporiate way.

(In fact, all CL expressions can be regarded as datatype trees too: CL is a total thing, we can us each CL expression in a same way as a datatype tree: we can apply it leaf- and branch-continuation arguments. Something will always happen. At worst it will diverge -- but lazy trees can diverge too, amd they are inarguably datatype trees. But now let us ignore all these facts, and let us define the notion of quotations in the restictive way: let the definition require to be structured in a predefined way.)

We use datatype trees for representing other expressions. Let us call CL expressions which can represent (another CL expreesion) quotations. Quotations are exactly the datatype trees, but

  • the world Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle quotation} refers to their function,
  • the world datatype tree refers to their implemetation, structure

This means a datatype tree

  • is not only a tree regarded only as a term tree,
  • but on a higher level: itself a recursive datatype implemented in CL, it is appropiately consisting of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{leaf}} ,Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{branch}} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{true}} , Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{false}} subexpressions so that we can reason about it in CL itself

How do quotations relate to all CL expressions?

  • In one direction, informally, we could say, quotations make a very proper subset of all CL expressions (attention: cardinality is the same!). Not every CL expressions are datatype trees.
  • But the reverse is not true: all CL expressions can be quoted! Foreach CL expressionther is a (unique) CL expression who quotes it!

We can define a quote function on the set of all CL expressions. But of it is an conceptually outside function, not a CL combinator itself! (that is why I do not typest it boldface. Is it an example of what Curry called epitheory?).

After having solved the representation (quoting) problem, we can do many things. We can define meta-concepts, e.g.

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \equiv} (the notion of same terms)
by bool tree equality
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle =} (equivalence made by reduction)
by building a metacircular interpreter

We can write our tutor program too. But let us discuss more clean and theoretical questions.

Concept of self-replication generalized -- pure functional quines[edit]

How can be the concept of quine transferred to combinatory logic? In the bellow definition, let us think of

  • Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A} 's as actions, programs
  • and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Q} 's as quotations, representations
A quine is a CL term Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A} this means quines are pure CL concepts, no imperative compromises
for whose normal form Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A_0} this means quines are Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle run}
there exists an equivalent CL-term Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Q} where datatypes in CL arealmost never defined in their normal form (not even ordered pairs are!). They save us from loosing information, but they almost never do that literary. I faced this as problems in nice rewritings when I wanted to implement CL with computer algebra services
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Q} is a quotation, which manifests itself in the fact that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Q} is a datatype tree (not only term tree) with boolean leafs,
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Q} quotes Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Q} is exactly the representation of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A}

So a quine is a program which is run, then rewrited as a quotation and so we get the representation of the original program.

Of course the first three requirements can be contracted in two. Thus, a quine is a CL-term which is equivalent to its own representation (if we mean representation as treated here).

A metacircular interpeter[edit]

We have seen that we can represent CL expressions in CL itself, which enables us to do some meta things (see the into of this section, especially Reflective programming, e.g. Reflection '96). The first idea could be: to implement CL in itself!

Implementing lazy evaluation[edit]

The most important subtask to achieve this goal is to implement the algorithm of lazy evaluation. I confess I simply lack almost any knowledge on algorithms for implementing lazy evaluation. In my Haskell programs, when they must implement lazy evaluation, I use the following hand-made algorithm.

Functions of increasing number of arguments pass the term tree to each other during analyzing it deaper and deaper. The functions are eval, apply, curry and lazy, but I renamed curry, because there is also a Prelude function (and a whole concept behind it) with the same name. So I chose Schönfinkel's name for naming the third function in this scheme -- it can be justified by the fact that Curry himself attributed the idea of currying to Moses Schönfinkel (but the idea is anticipated by Frege too). 

 module Reduce where
 
 import Term
 import Tree
 import BaseSym
 
 eval :: Term -> Term
 eval (Branch function argument) = apply function argument
 eval atom = atom
 
 apply :: Term -> Term -> Term
 apply (Branch f a) b = schonfinkel f a b
 apply atom argument = strictApply atom argument
 
 schonfinkel :: Term -> Term -> Term -> Term
 schonfinkel (Leaf K) f x = eval f
 schonfinkel (Branch f a) b c = lazy f a b c
 schonfinkel s a b = strictSchonfinkel s a b
 
 lazy :: Term -> Term -> Term -> Term -> Term
 lazy (Leaf S) c f x = schonfinkel c x (Branch f x)
 lazy k_or_compound x y z = schonfinkel k_or_compound x y `apply` z
 
 strictApply :: Term -> Term -> Term
 strictApply f a = f `Branch` eval a
 
 strictSchonfinkel :: Term -> Term -> Term -> Term
 strictSchonfinkel f a b = strictApply f a `strictApply` b
 module Term where
 
 import BaseSym
 import Tree

 type Term = Tree BaseSym
 type TermV = Tree (Either BaseSym Var)
 module Tree where
 
 data Tree a = Leaf a | Branch (Tree a) (Tree a)
 module BaseSym where
 
 data BaseSym = K | S
 type Var = String

and it seems hard to me hard to implement in CL. Almost all of these functions are mutual recursive definitions, and it looks hard for me to formulate the fixpont. Of coure I could find another algorithm. The main problem is that reducing CL trees is not so simple: the Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf S} rule requires lookahead in 2 levels. Maybe once I find another one with monads, arrows, or attribute grammars...

A lightweight CL implementation[edit]

I mean

  • instead of writing a CL interpreter (or compiler) with a huge amount of command-line arguments and colon-escaped prompt commands,
  • why not to write a lightweight library? (Lightweight in the sense as Parsec is lightweight in comparison to parser generators, or QuickCheck is lightweight).

This latter framework can contain the previous one e.g. by implementing 

interpreter :: IO ()
compiler :: Term -> Haskell

where Haskell can be a string, an appropriately designed abstract datatype, a rose tree or a Template Haskell term representation of Haskell expressions, thus any way used in Haskell metaprogramming (in the picture below, does it correspond to Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Term_{-\infty}} ?).

So, the latter can contain the former, but what are the new advantages? 

abstract :: Var -> TermV -> Maybe Term
abstractV :: Var -> TermV -> TermV
rewrite :: Term -> Reader Definitions (Tree (Either NonVar Definiendum))

where type Definitions = Map Definiendum Term. So we can get compiler algebra and other useful services in a modular way.

Of course also an interpreter can yield useful services, but as the user interface grows, it develops to have a command language, which is in most cases imperative having less gluing possibilities than being able to use Haskell itself by this lightweight approach.

In fact, it the was the quines (mentioned above) that forced me to think of a lightweight CL library instead of an interpreter. Writing a CL quine (in the way I can do) requires a lot of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathrm{quote}\!/\!_0} : quoting CL terms in CL itself. But quoting CL cannot be done in CL (only Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathrm{quote}\!/\!_1} : quoting-the-quotation-of-CL-further can be done in CL), so my CL quine plans needed a lot of work quoting CL terms by hand. A lightweight CL library could do this job by using the power of Haskell (quoting CL terms can be done in Haskell, or more generally said: in the ultimate implementating language of this CL-project).

The quotation stratification of subsequent series of meta- and object languages

The quotation stratification of subsequent series of meta- and object languages:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathrm{Term}_0\supset\mathrm{Term}_1\supset\mathrm{Term}_2\supset\dots}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathrm{Term}_0}
the ultimate implementing language of thus CL project (here Haskell)
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathrm{Term}_1}
combinatory logic, its terms being represented by Haskell binary tree abstract datatype.
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathrm{Term}_2}
combinatory logic, its terms being represented by combinatory logic binary tree abstract datatype. We have already seen that we can define lists in combinatory logic by catamorhisms, so we can define binary trees too. And we can represent the base combinators by booleans which can be defined too in CL. So we can quote each CL term in CL itself.
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathrm{Term}_2}
...

Quoting:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathrm{quote}/_0\in\mathrm{Term}_0} Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathrm{quote}/_0:\mathrm{Term}_1\to\mathrm{Term}_2}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathrm{quote}/_1\in\mathrm{Term}_1} Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathrm{quote}/_1:\mathrm{Term}_2\to\mathrm{Term}_3}

Invoking:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathrm{invoke}/_1\in\mathrm{Term}_1} Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathrm{invoke}/_1:\mathrm{Term}_2\to\mathrm{Term}_1} 
-- Yet we do not require type safety in quotation stratification of CL terms:
type Term1 = Term
type Term2 = Term
type Term3 = Term
-- ...
quote'0 :: Term1 -> Term2
quote'1_0 :: Term2 -> Term3
-- ...
-- At or beyond the depth of quote'1
-- these functions can be implemented in CL too
-- more generally: everyhing can be made at a higher level too,
-- but not vice versa. So everyhing has a grad
-- We index things by this grad
-- Ultimate implementing language (here:Haskell) is designed by grad 0
-- Unavailable grad is designed by minus infinity
-- (see the analogy of grad of polinomials)
quote'1 :: Term1
quote'2_1 :: Term1
quote'2 :: Term2

Illative combinatory logic[edit]

I think combinator Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf G} can be thought of as something analogous to Dependent type: it seems to me that the dependent type construct Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \forall x : S \Rightarrow T} of Epigram corresponds to Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf G\;S\;(\lambda x . T)} in Illative Combinatory Logic. I think e.g. the followings should correspond to each other:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf{realNullvector} :\;\;\;\forall n: \mathbf{Nat} \Rightarrow \mathbf{RealVector}\;n}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbf G\;\,\mathbf{Nat}\;\,\mathbf{RealVector}\;\,\mathbf{realNullvector}}


My dream is making something in Illative Combinatory Logic. Maybe it could be theoretical base for a functional logic language?

References[edit]

  • [Bun:NatICL] Martin W. Bunder: The naturalness of Illative Combinatory Logic as a Basis for Mathematics, see in Dedicated to H.B.Curry on the occasion of his 80th birthday.
Retrieved from "https://wiki.haskell.org/index.php?title=Combinatory_logic&oldid=41030"