\documentclass{article}
\usepackage{hyperref}
%include polycode.fmt
%lhs2TeX.fmt
%format :^: = ":\!\wedge\hspace{-0.5ex}:\mbox{}"
%format :*: = ":\!\times\hspace{-0.5ex}:\mbox{}"
%format :+: = ":\!+\hspace{-0.5ex}:\mbox{}"
%format ^ = "\wedge"
%format * = "\times"
%format ~ = "\sim"
%format <> = "\!\mathop{{}^{{}^{\cdot}}}\!"
%format :~: = ":" ~ ":"
\newcommand{\ZERO}{\!\mathop{{}^{{}^{\cdot}}}\!}
\title{The AMEN calculator}
\newcommand{\ie}{\textit{ie.\hspace{0.5ex}}}
\newcommand{\eg}{\textit{eg.\hspace{0.5ex}}}
\newcommand{\etc}{\textit{\&{}co.\hspace{0.5ex}}}
\newcommand{\logarythm}{$\lambda$og$_a$rhythm}
\begin{document}
\maketitle
\tableofcontents
\section{Benedictus benedicat}
Some haskell boilerplate. We are going to play around with
the ordinary arithmetical symbols, and versions of these
symbols in angle-brackets eg. |<+>|.
\begin{code}
module Arithmetic where
import Data.Char
import Prelude hiding
((*),(^),(+),(<>),(&),(~)
,(<*>),(<^>),(<+>),(<<>>),(<&>),(<~>)
,(:^:),(:*:),(:+:),(:<>:),(:&:),(:~:)
,pi
)
import Control.Applicative hiding ((<*>),empty)
infixr 8 ^
infixr 7 *
infixr 6 +
infixr 9 <>
infix 3 &
-- infix 3 ~ -- some weirdess about ~ as a symbol
help :: IO () -- Do something with this later.
help = let eg = " test $ vc :^: vb :^: va :^: cC " ; q = '"'
in putStrLn
("Load in ghci and type something like: " ++ (q:eg) ++ [q])
\end{code}
\section{Real-world arithmetical combinators}
Here are some simple definitions of binary operations corresponding to the
arithmetical combinators:
\begin{code}
a ^ b = b a
a * b = \c -> (c ^ a) ^ b
a + b = \c -> (c ^ a) * (c ^ b)
a `naught` b = b
-- some experiments
a & b = \c -> c a b
a ~ b = \c -> a c b -- |(a ~)| is a binary function with its arguments flipped.
\end{code}
Instead of |naught|, one can use the infix operator |(<>)|, that looks
a little like a `|0|'. It discards its left argument, and returns its right.
The type-schemes inferred for the definitions are as follows:
\begin{code}
(^) :: a -> (a -> b) -> b
(*) :: (a -> b) -> (b -> c) -> a -> c
(+) :: (a -> b -> c) -> (a -> c -> d) -> a -> b -> d
(<>) :: a -> b -> b
one :: a -> a
-- a couple of experiments
(&) :: a -> b -> (a -> b -> c) -> c
-- Following type declaration causes a parse error...
-- |(~) :: (a -> b -> c) -> b -> a -> c|
\end{code}
Anyone should think:
\begin{itemize}
\item continuation transform unit
\item action of contravariant functor |_ -> c| on morphisms
\item lifted version of the above
\item |const id|
\item |id|
\item pairing
\item flip
\end{itemize}
Here are the first few numbers
\begin{code}
(<>) = naught
zero = naught
one = zero ^ zero
suc n s = n s * s -- = (s ^ n) * (s ^ 1) = s ^ (n + 1)
two = suc one
three = suc two
four = two ^ two
five = two + three
six = two * three
seven = four + three
eight = two ^ three
nine = three ^ two
ten = two * five
\end{code}
Here they are in a list, with a common type.
\begin{code}
ff , nos :: [(a -> a) -> a -> a]
ff = [ zero,one,two,three,four
, five,six,seven,eight,nine,ten]
nos = zero: [ suc x | x <- nos]
\end{code}
\subsection{Infinitary operations: streams and lists}
For infinitary operations (this may come later) I might need
a few things.
The first folds a binary operation (such as addition)
over the finite prefixes of a stream. So |(x1,x2,x3, ... )|
is sent to |(0, x1, x1 + x2, x1 + x2 + x3, ... )|.
\begin{code}
pfs :: (a -> a -> a) -> a -> [a] -> [a]
pfs op ze xs = pfs' xs id
where pfs' (x:xs) b = b ze : pfs' xs (b . (op x))
\end{code}
|pfs| is applied only to streams, and returns a stream.
Think of it is a stream of finite lists, namely the list of finite
prefixes of the argumenty stream. Then we fold an operation over each list, starting
with a constant.
\begin{code}
type Endo x = x -> x
type N x = Endo (Endo x)
index :: N [a] -> [a] -> a
index n = (tail ^ n) * head -- head . n tail
-- note index 0 is head
sigma :: Endo [a -> Endo b]
pi :: Endo [ Endo a ]
pi = pfs (*) one
sigma = pfs (+) zero
\end{code}
Stuff related to continuations.
Should make monad instance etc.
\begin{code}
type C y x = (x -> y) -> y
ret :: x -> C y x
ret = (^)
mu :: C y (C y x) -> C y x
-- mu mm k = mm (ret k)
-- mu mm = ret * mm
mu = (^) ^ (*) -- ((^) * (^)) ^ flip
mp :: (a -> b) -> C y a -> C y b
mp = (*) * (*)
{- The types |x -> C x x| and |N x| are isomorphic. -}
{- The same combinator is used in both inverse directions! -}
myflip :: (x -> C x x) -> N x
myflip = flip
myflip' :: N x -> x -> C x x
myflip' = flip
\end{code}
I can't remember why I thought the below was interesting.
The argument of mydrop is a Church numeral.
\begin{code}
-- any of the following type statements will do
mydrop :: C y (Endo [a])
-- | mydrop :: (([a] -> [a]) -> t) -> t |
-- | mydrop :: (Endo [a] -> t) -> t |
-- | mydrop :: N [a] -> Endo [a] |
mydrop n = n tail
-- mydrop' = ($ tail)
\end{code}
\subsection{Booleans}
I wanted to look at Church encoding of booleans.
The following can all be restricted in such a way
that |a|, |b| and |c| are the same. This is analogous to
the situation with Church numerals.
\begin{code}
type I2 a b c = a -> b -> c
impB :: I2 (I2 a b c) (I2 b d a) (I2 b d c)
orB :: I2 (I2 a b c) (I2 a d b) (I2 a d c)
andB :: I2 (I2 a b c) (I2 d b a) (I2 d b c)
posB :: I2 a b a
nilB :: I2 a b b
impB a b p n = a (b p n) p
orB a b p n = a p (b p n) -- the same as numerical addition b + a
andB a b p n = a (b p n) n
posB = const
nilB = zero
if0 :: I2 a b c -> I2 b a c
ifP :: a -> a
ifP = id
if0 = flip
\end{code}
\section{Syntax for arithmetical expressions}
Arithmetical expressions are constructed using a signature with 4 binary operators,
and 4 constants.
\begin{itemize}
\item 4 constants |(^)|, |(*)|, |(+)| and |(<>)|
\item 4 binary operators |_^_|, |_*_|, |_+_| and |_<>_|
\end{itemize}
There is also an unlimited supply of fresh variables, named by strings (usually singleton characters).
An expression in which a variable occurs is said to be open, otherwise closed.
The defining equations for the arithmetical combinators generate two equivalence relations between
expressions. The first is `intensional': this is the least equivalence relation
extending the definitions, congruent to all operators in the signature.
This means that equations between open terms can be proved by
substituting equals for equals.
The second (more useful) equivalence relation identifies more expressions.
One can also allow instances of the so-called `$\zeta$-rule' in proving equations.
\begin{center}
\begin{tabular}{c} |x ^ a = x ^ b| $\mbox{}\Longrightarrow\mbox{}$ |a = b| \end{tabular}
\end{center}
with the side condition that |x| is fresh to both |a| and |b|.
The $\zeta$-rule is a cancellation law. It expresses
`exponentiality':
two expressions that behave the same as exponents of a generic base
(as it were, a cardboard-cutout of a base) are equivalent.
I call this equivalence relation $\zeta$-equality. Any equation herein
should be interpreted as a $\zeta$-equation, unless I explicitly say otherwise.
It may be that to determine the behaviour of an expression as an
exponent, we have to supply it with more than one base-variable.
Sometimes, `extra' variables play a role in allowing computations
to proceed, though subsequently these `extras' can be cancelled.
\section{Evaluating arithmetical expressions}
The arithmetical combinators are rather fascinating, but it is
easy to make mistakes when performing calculations.
We now write some code to explore on the computer
the evaluation of arithmetical expressions, built out
of our four/eight combinators.
First, here is a datatype |E| for arithmetical expressions. The symbols
for the constructors are chosen to suggest their interpretation as
combinators.
\begin{code}
infixr 9 :<>:
infixr 8 :^:
infixr 7 :*:
infixr 6 :+:
infixr 5 :&:
infixr 5 :~:
\end{code}
\begin{code}
data E = V String
| C String -- experiment
| E :^: E
| E :*: E
| E :+: E
| E :<>: E -- indirection
| E :~: E -- flip (experiment)
| E :&: E -- pairing (experiment)
deriving (Eq) -- (Show,Eq)
\end{code}
We can think of these expressions as fancy Lisp S-expressions, with four
different binary `cons' operations, each with an distinct arithmetical flavour.
As for the experiments, we can define |&| and |~| by
\begin{spec}
(a ~ b) = a * (b ^)
(a & b) = (a ^) * (b ^)
\end{spec}
It is convenient to have atomic constants/combinators identified by symbolic strings.
The constants |"+"|, |"*"|, |"^"|, |"0"|, |"1"| (among others) are treated specially.
\begin{code}
( cA, cM, cE, cN)
= ( V"+", V"*", V"^", V"0")
cI = cN :^: cN
( c0, c1 ) = (cN, V "1")
\end{code}
It is convenient to have symbols for the flipped versions:
\begin{code}
( cAcC, cMcC, cEcC, cNcC) =
let f = ('~':) * V -- this is typeset very wierdly
in ( f "+", f "*", f "^" , f "0" )
cB_possible = cMcC
cK_possible = cNcC
cI_possible = cEcC
\end{code}
\iffalse
% , V"<>" -- discard left-hand argument
%-- cC, cCcC,
%-- cPair , cPaircC,
%-- , V"~" , V "~~" -- flip ; rotR a b c - b c a (store)
%-- , V"&" , V $~&" -- rotL. reverse exchanges 1 and 3.
\fi
Now we turn to evaluation of expressions. Of course, this will be
only a partial function, as there are expressions which one
cannot be completely evaluated.
To begin with, we disregard reduction sequences, and focus on
the value returned by a terminated sequence. (We'll consider reduction sequences in a moment.)
For each binary arithmetical operator, we define a function that takes two
arguments, and (sometimes) returns a `normal' form of the expression
formed with that operator. Then we recurse (in |eval|) over the structure of an expression
to define the code that might return its normal form.
I'm not entirely confident the following works properly.
It should match the |tlr| given later.
\begin{code}
infixr 9 <<>>
infixr 8 <^>
infixr 7 <*>
infixr 6 <+>
\end{code}
\begin{spec}
infixr 5 <&> -- oh... I doubt |<,>| is available...
infixl 4 <~>
\end{spec}
\begin{code}
(<+>),(<*>),(<^>),(<<>>) :: E -> E -> E
a <+> b = case a of
V"0" -> b
_ -> case b of
V"0" -> a
b1 :+: b2 -> (a <+> b1) <+> b2
_ -> a :+: b
a <*> b = case a of
V"1" -> b
_ :^: V"0" -> b
_ -> case b of
V"0" -> b
b1 :+: b2 -> (a <*> b1) <+> (a <*> b2)
b1 :*: b2 -> (a <*> b1) <*> b2
V"1" -> a
V"0" :^: V"+" -> a
V"1" :^: V"*" -> a
_ :^: V"0" -> a
_ -> a :*: b
a <^> b = case b of
V"0" -> V"1" -- b :^: b
V"1" -> a
b1 :+: b2 -> (a <^> b1) <*> (a <^> b2)
b1 :*: b2 -> (a <^> b1) <^> b2
V"0" :^: V"+" -> a
V"1" :^: V"*" -> a
_ :^: V"0" -> a
b1 :^: V"^" -> b1 <^> a -- note: destroys termination
b1 :^: V"*" -> case b1 of { V"1" -> a ; _ :^: V"0" -> a ; _ -> b1 <*> a}
b1 :^: V"+" -> case b1 of { V"0" -> a ; _ -> b1 <+> a}
b1 :^: b2 -> a :^: (b1 <^> b2)
_ -> a :^: b
_ <<>> b = b
\end{code}
The following (partial!) function then evaluates an arithmetic
expression.
\begin{code}
eval :: E -> E
eval a = case a of b1 :+: b2 -> eval b1 <+> eval b2
b1 :*: b2 -> eval b1 <*> eval b2
b1 :^: b2 -> eval b1 <^> eval b2
_ :<>: b2 -> eval b2
_ -> a
\end{code}
This first piece of code is an evaluator, that computes the normal form
of an expression (with respect to some rewriting rules hard-wired in the code),
unless it "hangs", or consumes all the memory in your computer.)
Such an evaluator may let look at the normal form of an expression, if it has one.
but it doesn't show how this was arrived at. (This is done below.)
There are various systems and reduction strategies of interest. They
arise from the algebraic structure: the additive and multiplicative
monoids, weak distributivity, etc.
\section{Rewriting arithmetical expressions}
If an expression does not have a value, then the |eval| function
of the last section will not produce one, thank heavens. Nevertheless, one
may want to observe finite segments of the sequence of reductions.
The second piece of code is for watching the reduction
rules in action.
The machinery is controlled by a single (case-)table of
contractions (ie. top-level reductions), in the function |tlr| below.
This maps an expression to the list of expressions to which it
can be reduced in one top-level step (rewriting the root of the expression).
To vary the details of reduction, one can tinker with the definition
of |tlr|.
Although the lists returned here are at most singletons, in other variants
there might be overlap: more than one reduction rule might apply. In such a case,
the order of pattern matching might matter.
\begin{code}
tlr :: E -> [E]
tlr e = case e of
-- addition |+|
(a :+: (b :+: c)) -> [ (a :+: b) :+: c ] -- space reuse
(V "0" :+: a) -> [ a ] -- drop1
(a :+: V "0") -> [ a ] -- drop1
-- multiplication |*|
(a :*: (b :+: c)) -> [ (a :*: b) :+: (a :*: c) ] -- 2 to 3
(a :*: V "0") -> [ c0 ] -- drop1
(a :*: (b :*: c)) -> [ (a :*: b) :*: c ] -- reuse
(a :*: V "1") -> [ a ] -- drop1
(V "1" :*: a) -> [ a ] -- drop1
-- random |*| optimisations
(V "*" :*: (V "^" :^: V "*")) -> [ V "~" ] -- EXPERIMENT!!
((a :*: V "*") :*: (V "^" :^: V "*")) -> [ a :*: V "~" ] -- EXPERIMENT!! re reassociate
(V "~" :*: V "~") -> [ c1 ] -- missing a square root, I think
(V "^" :*: V "~") -> [ V "&" ] -- apparently.
(V "&" :*: V "~") -> [ V "^" ] -- apparently. Others?
--
-- exponentiation |^|
(a :^: (b :+: c)) -> [ (a :^: b) :*: (a :^: c) ] -- 2 to 3
(a :^: V "0") -> [ c1 ] -- drop1
(a :^: (b :*: c)) -> [ (a :^: b) :^: c ] -- reuse
(a :^: V "1") -> [ a ] -- drop1 -- idle
-- random |^| optimisations
(V "^" :^: V "~") -> [ c1 ] -- strong eta
(V "0" :^: V "+") -> [ c1 ] -- |0/1| left units for |+/*|
(V "1" :^: V "*") -> [ c1 ]
--
(a :^: b :^: V "+") -> [ b :+: a ] -- drop1
(a :^: b :^: V "*") -> [ b :*: a ] -- drop1
(a :^: b :^: V "^") -> [ b :^: a ] -- drop1 -- top 2 swap
(a :^: b :^: V "0") -> [ b :<>: a ] -- drop1 -- indirection
(a :^: b :^: V "~") -> [ b :~: a ] --
(a :^: b :^: V "&") -> [ b :&: a ] --
(a :^: b :^: V "~+") -> [ a :+: b ] -- drop1
(a :^: b :^: V "~*") -> [ a :*: b ] -- drop1
(a :^: b :^: V "~^") -> [ a :^: b ] -- drop1 -- top 2 swap
(a :^: b :^: V "~0") -> [ a :<>: b ] -- drop1 -- indirection
(a :^: b :^: V "~~") -> [ a :~: b ] --
(a :^: b :^: V "~&") -> [ a :&: b ] --
(a :^: (b :&: c)) -> [ c :^: b :^: a ] -- a 2-chain
(a :^: (b :~: c)) -> [ c :^: a :^: b ] -- a 3-chain
-- naught
(_ :<>: b) -> [ b ] -- drop1
-- nothing else is reducible
_ -> [ ]
\end{code}
Thought: the associativity laws can be done in place.
The distribution laws cannot. Quite a few others can reuse the
redex as an indirection node.
To represent subexpressions, we use a `zipper', in a form in which the
context of a subexpression is represented by a linear function. We
represent each part |e| of an expression |e'| (at a particular
position) as a pair |(f,e)| consisting of the subexpression |e| there,
and a linear function |f| such that |f e = e'|. (By construction, the
function is linear in the sense that it uses its argument exactly
once.) Intuitively you `plug' the subexpression |e| into the `context'
|f| to get back |e'|.
The function |sites| returns (in top down preorder: root, right, left \ldots)
all the subexpressions of a given expression, together with the
one-hole contexts in which they occur. This includes the improper case of
the expression itself in the empty context. I represent the one-hole contexts
by a composition of functions that when applied to the contextualised part
will return the outermost expression.
\begin{code}
sites :: E -> [(E->E,E)]
sites e = (id,e) : case e of
(a :+: b) -> h (:+:) a b
(a :*: b) -> h (:*:) a b
(a :^: b) -> h (:^:) a b
(a :&: b) -> h (:&:) a b
(a :~: b) -> h (:~:) a b
(a :<>: b) -> sites b -- DANGER! indirection
_ -> [] -- no internal sites
where
h o a b = i ++ ii where
i = [ ((a `o`) . f,p) | (f,p) <- sites b ] -- right operand b first
ii = [ ((`o` b) . f,p) | (f,p) <- sites a ]
\end{code}
A variant. %| sites e = [ (composelist fs,p) | (fs,p) <- sites' e ] |
\begin{code}
-- sites' :: E -> [([E->E],E)]
sites' e = ([],e) : case e of
(a :+: b) -> h cA a b
(a :*: b) -> h cM a b
(a :^: b) -> h cE a b
(a :&: b) -> h cPair a b
(a :~: b) -> h cC a b
(a :<>: b) -> sites' b -- DANGER! indirection
_ -> [] -- no internal sites
where
h o a b = i ++ ii
where
i = [ ((a :^: o) : f,p) | (f,p) <- sites' b ] -- right operand b first
ii = [ ((b :^: o :^: cC) : f,p) | (f,p) <- sites' a ]
\end{code}
Quick hack towards linear logs.
\begin{code}
lblog vn e = head [foldr (:*:) c1 (reverse fs) | (fs,p) <- sites' e, p == V vn]
\end{code}
It should be noted that `far-right' sites are prioritised. This mirrors the
normal situation, where the left comes first.
A criticism of the above code is that it might be more useful to
keep a \emph{list} of off-path expressions (rather than the
composite of functions like |(o a)| and |(flip o a)|). In
a linear logarithm, we want to replace composition with
multiplication.
Now we define for any expression a list of the expressions to which it
reduces in a single, possibly internal step, at exactly one site
in the expression. This uses the function |tlr| to get
top-level reducts.
\begin{code}
reducts :: E -> [ E ]
reducts a = [ f a'' | (f,a') <- sites a, a'' <- tlr a' ]
\end{code}
\subsection{The tree of reduction sequences, and access to it}
We need a structure to hold the reduction sequences from an
expression. So-called `rose' trees, with nodes labelled with
expressions seem ideal.
\begin{code}
data Tree a = Node a [ Tree a ] deriving Show
\end{code}
We define a function which maps an expression to its tree of
reduction sequences.
\begin{code}
reductTree :: E -> Tree E
reductTree e = Node e [ reductTree e' | e' <- reducts e ]
\end{code}
The following function maps a tree to
a sequence enumerating the nonempty sequences of
node labels encountered on a path from the root of the tree to a (leaf) node without descendants.
\begin{code}
branches :: Tree a -> [[a]]
branches (Node a []) = [ [a] ]
branches (Node a ts) = [ a : b | t <- ts, b <- branches t]
\end{code}
Putting things together, we can map an expression to
a sequence of its reduction sequences. (Hence |rss|.)
\begin{code}
rss :: E -> [[E]]
rss = branches . reductTree
\end{code}
The first `canonical' reduction sequence in my enumeration seems
top-down, or lazy in some sense. It is usually
quite usable (to understand what is going on in a calculation),
at least by me.
\section{B{\"o}hm's \logarythm}
This code constructs the \logarythm{} of an expression
with respect to a variable name.
B{\"o}hm's combinators. Check carefully!!
\begin{code}
cBohmA a b = let curry g = cPair :+: g :^: cK in -- additive
let curry' g = cPair :*: cM :*: (g :^: cE) -- multiplicative
in curry' (a :^: cE :+: b :^: cE)
cBohmE a b = a :*: cPair :+: b :*: cE
cBohmE' a b = b :*: cC :+: a :*: cE
cBohmM a b = a :+: b
cBohm0' a = c0 :~: a
cBohm0 a = c0 :*: (a :^: cE)
cBohmC a b = a :+: b :*: cE -- I had cC instead of cE!
cBohmP a b = a :*: cE :+: b :*: cE -- pairing
\end{code}
These have the crucial properties
\begin{spec}
x ^ cBohmA a b = (x ^ a) + (x ^ b)
x ^ cBohmM a b = (x ^ a) * (x ^ b)
x ^ cBohmE a b = (x ^ a) ^ x ^ b
x ^ cBohm0 a = a
x ^ cBohmP a b = ( x ^ a , x ^ b )
x ^ cBohmC a b = ( x ^ a ~ x ^ b )
\end{spec}
used in defining the logarithm.
The code below can perhaps refined to keep the size
of its logarithms down. It is very naive.
The interesting cases are those where
the variable occurs in just once of a pair of operands.
I am about to change this, so I'll try to clarify my thoughts.
I intend to treat \emph{linear} logarithms explicitly as a special case.
With linear logarithms, when searching for the single
occurrence of the variable, we accumulate a list of functions $[f_1, \dots f_n]$,
the composition of which (in one direction or another) is a function that sends an given expression
to the top-level expression with the variable occurrence replaced by an occurrence of the given expression.
The logarithm in this case is a certain product.
The functions are left or right sections of a binary operator:
| (a `o`)| or |(`o` a)| -- which can be written | (`~o` a)|,
if |`~o`| is the flipped version of |`o`|.
Now we form the linear log as the product
\[
f_1^{o_1} \times \ldots \times f_n^{o_n}
\]
\begin{code}
blog v e | not (v `elem` fvs e) = cBohm0 e
blog v e =
case e of
a :+: b -> case (v `elem` fvs a,v `elem` fvs b) of
(False,True) -> (blog v b) :*: (a :^: cA)
(True,False) -> (blog v a) :*: (b :^: cA :^: cC)
_ -> cBohmA (blog v a) (blog v b)
a :*: b -> case (v `elem` fvs a, v `elem` fvs b) of
(False,True) -> (blog v b) :*: (a :^: cM)
(True,False) -> (blog v a) :*: (b :^: cB)
_ -> cBohmM (blog v a) (blog v b)
a :^: b -> case (v `elem` fvs a, v `elem` fvs b) of
(False,True) -> case b of
V v -> a :^: cE
_ -> blog v b :*: (a :^: cE)
(True,False) -> case a of
V v -> b
_ -> blog v a :*: b
_ -> cBohmE' (blog v a) (blog v b)
a :~: b -> cBohmC (blog v a) (blog v b)
a :&: b -> cBohmP (blog v a) (blog v b)
V nm -> if nm == v then c1 else cBohm0 e
\end{code}
\iffalse
{-
\begin{spec}
let
x = [(f,t) | (f,t) <- sites e, t == V v ]
in case x of
[(f,t)] -> -- single occurrence
[] -> -- does not occur
_ -> -- multiple occurrences
\end{spec}
-}
\fi
The following function returns a list of all the variable names occurring in an expression.
The list is returned in the order in which variables are encountered in a depth-first scan.
\begin{code}
fvs e = nodups $ f e []
where f (V nm) = if nm `elem` [ "0", "1", "^", "*", "+",
"$", ",", "~", ".", "&" ]
then id else (nm:)
-- NB: |,| is just |&| (pairing).
-- |.| is reverse |*| (unused)
-- |$| is reverse |^| (unused)
f (a :^: b) = f a . f b
f (a :*: b) = f a . f b
f (a :+: b) = f a . f b
f (a :<>: b) = f b -- we regard position a as junk
f (a :~: b) = f a . f b
f (a :&: b) = f a . f b
\end{code}
It has to be said that `$x$ occurs in $a$' is merely a sufficient, but not
a necessary condition for $a$ to be independent of $x$. Consider | vx :^: c0 |.
\appendix
\section{Bureaucracy and gadgetry}
To save typing, names for all single-letter variables
\begin{code}
( va, vb, vc, vd, ve, vf, vg, vh,
vi, vj, vk, vl, vm, vn, vo, vp,
vq, vr, vs, vt, vu, vv, vw, vx, vy, vz)
= ( V"a", V"b", V"c", V"d", V"e", V"f", V"g", V"h",
V"i", V"j", V"k", V"l", V"m", V"n", V"o", V"p",
V"q", V"r", V"s", V"t", V"u", V"v", V"w", V"x", V"y", V"z")
\end{code}
We code a few useful numbers as expressions.
\begin{code}
c2, c3, c4 , c5, c6, c7, c8, c9, c10 :: E
(c2,c3,c4) = (c1 :+: c1, c2 :+: c1, c2 :^: c2)
(c5,c6,c7) = (c3 :+: c2, c3 :*: c2, c3 :+: c4)
(c8,c9,c10) = (c2 :^: c3, c3 :^: c2, c2 :*: c5)
\end{code}
|c0| and |c1| have already been defined.
It is time we had an combinator for successor ($(+) \times 1^{(\wedge)}$, by the way).
\begin{code}
cSuc :: E
cSuc = blog "x" (vx :+: c1)
chN :: Int -> E -- allows inputting numerals in decimal.
chN n = let x = c0 : [ t :+: c1 | t <- x ] in x !! n
chN_suggestion = "test $ vz :^: vs :^: cN 7"
\end{code}
Luckily, we can print real church numerals in decimal,
and therefore print the first few values of a
function of type | Endo (Endo (Endo a)) |
\begin{code}
base10 :: Endo (Endo Int) -> Int
base10 n = n succ 0
ffv_suggestion = "let eg n = (n * n) + n in map (base10 . eg) ff "
\end{code}
Note that all terms are divisible by 2.
(Division by two is a tricky matter...)
\newpage
\section{Displaying}
\subsection{Expressions}
If one wants to investigate reduction sequences of arithmetical
expressions by running this code, one needs to display them.
To display expressions, we use the following code,
which is slightly less noisy than the built in show instance.
It should supress parentheses with associative operators, so
sometimes the same expression appears to be repeated.
(I think everything is right associative: as with |^|, so
with the other operators.)
I write the constant combinators in square brackets, which may
be considered noisy.
Actually, it might be more useful for printing to use one
level of superscripts, as when type-setting latex code.
There is at least half a chance of a human being making out
some structure in a string of arithmetical gibberish.
I don't understand precedences very well. I think the following
deals properly with associativity of |+| and |*|, and their
relative precedences (sums of products) but
also with the non-associativity of |^|. These nest to the right.
The best I can say is that by some miracle it seems to work as I expect.
\begin{code}
showE :: E -> Int -> String -> String
showE (V "^") _ = ("[^]"++)
showE (V "*") _ = ("[*]"++)
showE (V "+") _ = ("[+]"++)
showE (V ",") _ = ("[,]"++)
showE (V "~") _ = ("[~]"++)
showE (V "&") _ = ("[&]"++)
showE (C "^") _ = ("[^]"++)
showE (C "*") _ = ("[*]"++)
showE (C "+") _ = ("[+]"++)
showE (C ",") _ = ("[,]"++)
showE (C "~") _ = ("[~]"++)
showE (C "&") _ = ("[&]"++)
showE (V str) _ = (str++)
showE (a :+: b) p = opp p 0 (showE a 0 . (" + "++) . showE b 0)
showE (a :*: b) p = opp p 2 (showE a 2 . (" * "++) . showE b 2)
showE (a :^: b) p = opp p 4 (showE a 5 . (" ^ "++) . showE b 4)
-- because the below are wierd operators, I write them noisily.
showE (a :<>: b) p = opp p 4 (showE a 5 . (" "++) . showE b 4)
showE (a :~: b) p = opp p 4 (showE a 5 . (" <~> "++) . showE b 4)
showE (a :&: b) p = opp p 4 (showE a 5 . (" <&> "++) . showE b 4)
parenthesize f = showString"(" . f . showString")"
opp p op = if p > op then parenthesize else id
\end{code}
\begin{code}
instance Show E where showsPrec _ e = showE e 0
\end{code}
\subsection{Trees and lists}
Code to display a numbered list of showable things, throwing a line between entries.
\begin{code}
newtype NList a = NList [a]
instance Show a => Show (NList a) where
showsPrec _ (NList es) =
(composelist . commafy ('\n':) . map showline . enum ) es
where showline (n,e) = shows n . showString ": " . shows e
\end{code}
\subsubsection{General list and stream amenities}
Code to pair each entry in a list/stream with its position.
\begin{code}
enum :: [a] -> [(Int,a)]
enum = zip [1..]
\end{code}
Code to compose a finite list of endofunctions.
\begin{code}
composelist :: [ a -> a ] -> a -> a
composelist = foldr (.) id
\end{code}
Code to insert a `comma' at intervening positions in a stream.
\begin{code}
commafy :: a -> [a] -> [a]
commafy c (x:(xs'@( _ : _ ))) = x:c:commafy c xs'
commafy c xs = xs
\end{code}
Remove duplicates from a list/stream. The order in which entries are
first encountered is preserved in the output.
\begin{code}
nodups :: Eq a => [a] -> [a]
nodups [] = []
nodups (x:xs) = x : filter (/= x) (nodups xs) {-
let xs' = nodups xs in
if x `elem` xs'
then del1 x xs' id -- filter (/= x) xs'
else xs'
-}
-- delete exactly one occurrence of first argument in second
del1 c (c':cs) | c == c' = (cs ^) -- only invoked when c actually occurs
del1 c (c':cs) = \ b -> del1 c cs (b . (c' :))
\end{code}
\subsection{Some top-level commands}
The first reduction sequence. This is usually the most useful. One might type something like
\begin{spec}
test $ vu :^: vz :^: vy :^: vx :^: cS
\end{spec}
\begin{code}
test :: E -> NList E
test = NList . head . rss
\end{code}
The normal form. This is occasionally useful when evaluation will obviously
terminate. Only the normal form is displayed.
\begin{spec}
eval $ vz :^: vy :^: vx :^: cS
\end{spec}
Display the n'th reduction sequence in a reduction tree.
\begin{code}
nth_rs :: Int -> E -> NList E
nth_rs n = NList . (!! n) . rss
\end{code}
Display an entire |NTree a|. Uses indentation in an attempt to make the
branching structure of the tree visible.
(Actually, this is almost entirely useless, except for very small expressions)
\begin{code}
newtype NTree a = NTree (Tree a)
instance Show a => Show (NTree a) where
showsPrec p (NTree t) =
f id (1,t) where -- | f :: Show a => ShowS -> (Int,Tree a) -> ShowS |
f pr (n,Node a ts)
= (pr -- emit indentation
. showString "["
. shows n
. showString "] " -- child number
. shows a -- node label
. showString "\n"
. ( composelist
. map (f (pr . showString "! "))
. enum ) ts)
\end{code}
We can try something like | let s = Ntree .reductTree in s (va :^: cS) |.
Some basic stats on reduction sequence length. The number
of reduction sequences, and the extreme values of their lengths.
Be warned, this can take a very long time to finish on
even quite small examples.
\begin{code}
stats_rss :: E -> (Int,(Int,Int))
stats_rss e = let (b0:bs) = map length (rss e)
in (length (b0:bs), ( foldr min b0 bs , foldr max b0 bs) )
data DisplayStats = DisplayStats (Int,(Int,Int))
instance Show (DisplayStats) where
showsPrec _ (DisplayStats (n,(l,h)))
= ("There are "++) . shows n . (" reduction sequences"++)
. (", varying in length between "++)
. shows l . (" and "++) . shows h
\end{code}
\begin{code}
-- check that all reduction sequences terminate with the same expression
nf :: E -> [E]
nf = map last . rss
-- might be useful
-- find the first suffix of a list that begins with a change
fd :: [E] -> Maybe [E] -- first difference
fd [] = Nothing
fd [x] = Nothing
fd (x:xs@(y:_)) | x == y = fd xs
fd z@(x:xs@(y:_)) | x /= y = Just z
-- do not try this on a constant infinite stream.
\end{code}
\subsection{IO}
We might contemplate running these programs,
as opposed to just evaluating them.
My suggestion is to think of the programs as
stream processors.
In this situation, the program can contain
at most one occurrence each of two special
variables, that are treated specially by the
execution system. Linearity of these
occurrences is extremely important here.
The program runs in a state-space consisting
of an accumulator register (containing maybe
an expression), and an unconsumed stream of
items from some stream type. For simplicity,
let us say the output also has the same type.
Two possibilities:
\begin{itemize}
\item tokens, as recognised by a scanner.
\item entire arithmetical expressions.
\end{itemize}
Each execution cycle of the program consumes
some initial segment (possibly null) of the input stream (stdin),
by finitely often reading items successively from it, and
atomically performs a corresponding action based on
the content of the accumulator.
(This might be to make it available on stdout.)
One can imagine two variables, or IO-combinators: |Rd| and |Wr|,
at which evaluation gets stuck (in hnf with those heads).
In the former case, an item is consumed, and passed as an
argument to the function that is the combinator's argument,
for further evaluation.
In the latter case, the combinator's argument is appended to stdout.
(A table needed.)
The machine's state space is: |(control,stdin,stdout)|.
Its transitions are tabulated from left to right below.
\begin{center}
\newcommand{\vvec}[1]{\ensuremath{\left(\begin{array}{l} #1 \end{array}\right)}}
\begin{tabular}{ll}
%\textit{hnf} &
\textit{\underline{state}} & \textit{\underline{state'}} \\[1ex]
%| disp :^: Rd | &
$\vvec{
|disp :^: Rd| \\
|item :&: stdin| \\
|stdout|
}$
& $\vvec{
|item :^: disp| \\
|stdin| \\
|stdout|
}$
\\[2em]
%| (item :&: nxt) :^: Wr | &
$\vvec{
| (item :&: nxt) :^: Wr | \\
| stdin | \\
| stdout |
}$
& $\vvec{
|nxt| \\
|stdin| \\
|stdout :&: item|
}$
\end{tabular}
\end{center}
The control state is really a cursor into an arithmetical expression.
I just show the subexpression in focus.
The stream of output produced by the program is then
a potentially infinite history of items successively
written to stdout.
The history of input consumed by the program is then
a finite history of successively read stdin items.
(Or something similar ...)
\iffalse
\begin{code}
elim :: [a] -> (a,[a])
elim ts = (head ts, tail ts)
-- step_add' (a,f) = (a + f o, f . s)
-- step_mul' (a,f) = (a * f o, f . s)
step_add (a,f) = (a + head f, tail f)
step_mul (a,f) = (a * head f, tail f)
-- step f (a,w) = (f a (head w), tail w)
-- f a i = a . (i:)
step (b,w) = (b . (head w:), tail w)
postprocess b = b []
-- run :: X^w -> (E . E) (E (X^*),X^w) -> A^w
run inp n =
post . iteration n -- (n step start)
where
-- step :: (E (X^*), X^w) -> (E (X^*), X^w)
step (b,w) = ( tack b (head w:) , tail w )
-- start :: (E (X^*), X^w)
start = (empty,inp)
-- empty :: E (X^*)
empty = id
-- tack :: E (X^*) -> X -> E (X^*)
tack b x = b . x -- tack = (.)
-- emit :: E (X^*) -> X^*
emit b = b [] -- emit = ($[])
post = id -- just for example
-- post :: X^* -> A -- some kind of fold
-- iteration :: (E . E) (E (X^*),X^w) -> (E (X^*),X^w)
iteration n = n step start
\end{code}
\fi
\newpage
\section{Parsing}
Is it even worth thinking about this? The interpreter gives a
fine language for defining expressions, using let expressions, etc.
Something changed in ghc 7.10.2 making it a fuss to write simple parsers.
Applicative is bound up with monads, and they have stolen |<*>|. If
I hide that, I hide monads, and can't use do notation.
\subsection{(parsing) combinators}
Choice: brain-dead parsing monad.
I don't understand the beaurocracy of instance declarations
well enough to use it properly.
Doesn't deal with input using pairing and flipping.
To be honest, I'm not sure how how precedences
and associativity should go with these operators.
(This means, with expressions like | a & b | and | a ~ b |.)
\begin{code}
-- import Control.Applicative
-- PARSERS.
-- t is the token type, v the parsed value.
newtype Parser t v = P {prun :: [t] -> [(v,[t])]}
instance Functor (Parser t) where
fmap f (P pr) = P (\ ts -> [ (f v, ts') | (v,ts') <- pr ts])
instance Applicative (Parser t) where
pure t = P (\ ts -> [(t,ts)])
liftA2 = fby2'
instance Monad (Parser t) where
return = eta
a >>= b = mmul (fmap b a) -- P (\ ts-> mmul (fmap b a))
\end{code}
\iffalse
{-
instance Monad (Parser t) where
return = eta
a >>= b = Parser (\ ts-> mmul (fmap b a))
-}
\fi
\begin{code}
eta :: v -> Parser t v -- pure
eta v = P (\ ts -> [(v,ts)])
mmul :: Parser t (Parser t v) -> Parser t v
mmul pp = P (\ ts -> [(v,ts'') | (p,ts') <- prun pp ts, (v,ts'') <- prun p ts'] )
sat :: (t -> Bool) -> Parser t t
sat p = P f where f (t:ts) | p t = [(t,ts)]
f _ = []
lit :: Eq t => t -> Parser t t
lit t = sat (== t)
-- composes a sequence of N parsers that return things of the same type A
-- into a parser that returns a list in A* of length N.
fby :: Parser t a -> Parser t [a] -> Parser t [a]
fby = liftA2 (:)
fby2 :: Parser t a -> Parser t b -> (a -> b -> c) -> Parser t c
fby2 p q f
= P (\s-> [ (f v v',s'') | (v,s') <- prun p s
, (v',s'') <- prun q s' ])
fby2' :: (a -> b -> c) -> Parser t a -> Parser t b -> Parser t c
fby2' f p q = fby2 p q f
grdl :: Parser t a -> Parser t b -> Parser t b
grdr :: Parser t a -> Parser t b -> Parser t a
grdl' p q
= P (\s-> [ (b,s'') | (_,s') <- prun p s, (b,s'') <- prun q s' ])
grdl = fby2' (flip const)
grdr' p q
= P (\s-> [ (a,s'') | (a,s') <- prun p s, (_,s'') <- prun q s' ])
grdr = fby2' const
paren' p = P (\s-> [ (a,s''')
| (_,s') <- prun (lit Lpar) s
, (a,s'') <- prun p s'
, (_,s''') <- prun (lit Rpar) s''])
paren p = grdl (lit Lpar) (grdr p (lit Rpar))
alt :: Parser t a -> Parser t a -> Parser t a
alt p q = P (\s-> prun p s ++ prun q s)
alts :: [Parser t a] -> Parser t a
alts ps = P (\s->concat [ prun p s | p <- ps ])
empty :: Parser t [a]
empty = P (\s->[([],s)])
rep, rep1 :: Parser t a -> Parser t [a]
rep p = rep1 p `alt` empty
rep1 p = p `fby` rep p
repsep :: Parser t a -> Parser t b -> Parser t [a]
repsep p sep = p `fby` rep (sep `grdl` p)
\end{code}
\subsection{scanner}
A token is given by a string (possibly empty) of non-blank characters.
Two are the parentheses. Some of these are identifiers, that start with a
letter, and then proceed in some nice subset of the non-blank characters.
The rest, more or less, apart from the parentheses are deemed symbol tokens.
One of the token types is |Num|. This is an unused placeholder.
\begin{code}
-- |tokens| turns a stream of characters into a stream of tokens.
is_alphabetic c = 'a' <= (c :: Char) && c <= 'z' || 'A' <= c && c <= 'Z'
is_digit c = '0' <= (c :: Char) && c <= '9'
is_idch c = c `elem` "_." || is_alphabetic c || is_digit c
is_space c = c == ' '
is_par c = c `elem` "()"
is_symch c = not (is_par c || is_space c)
data Tok = Id String | Num Int |
Sym String | Lpar | Rpar
deriving (Show,Eq)
tokens :: String -> [Tok]
tokens [] = []
tokens (c:cs) | isSpace c = tokens cs
tokens (inp@('(':cs))
= Lpar : tokens cs
tokens (inp@(')':cs))
= Rpar : tokens cs
tokens ('[':cs) -- hack to allow reading what I print
= id_t id cs where
id_t b [] = [Sym (b [])]
id_t b (']':cs) = Sym (b []): tokens cs
id_t b (c:cs) = id_t (b . (c :)) cs
tokens (c:cs) | is_alphabetic c
= id_t (c:) cs where
id_t b [] = [Id (b [])]
id_t b (c:cs) | is_idch c = id_t (b . (c :)) cs
id_t b inp = Id (b []): tokens inp
tokens (c:cs)
= id_t (c:) cs where
id_t b [] = [Sym (b [])]
id_t b (c:cs) | is_symch c = id_t (b . (c :)) cs
id_t b inp = Sym (b []): tokens inp
\end{code}
\subsection{rudimentary grammar}
\begin{code}
variable, constant, atomic :: Parser Tok E
variable = P p where
p (Id st : ts) = [(V st,ts)]
p _ = []
constant = P p where
p (Sym st : ts) = [(V st,ts)]
p _ = []
atomic = variable `alt` constant `alt` paren expression
additive, multiplicative, exponential, expression, discard :: Parser Tok E
additive = P ( \s->
[ (fo (:+:) x xs ,s')
| ((x:xs),s') <-
prun (repsep multiplicative (lit (Sym "+"))) s ])
multiplicative = P ( \s->
[ (fo (:*:) x xs ,s')
| ((x:xs),s') <-
prun (repsep exponential (lit (Sym "*"))) s ])
exponential = P ( \s->
[ (fo (:^:) x xs ,s')
| ((x:xs),s') <-
prun (repsep atomic (lit (Sym "^"))) s ])
-- twiddles??
-- pairs??
expression = additive
discard = P (\s-> [ (fo (:<>:) x xs ,s')
| ((x:xs),s') <-
prun (repsep atomic
((lit (Sym "!"))
`alt` lit (Sym "<>"))) s
])
\end{code}
I'm unsure which of these `fold' operators to use.
I may have just broken the parser!
\begin{code}
fo op s [] = s
fo op s (x:xs) = s `op` fo op x xs
fo' op s [] = s -- tail recursive
fo' op s (x:xs) = fo' op (s `op` x) xs
\end{code}
Useful to test parsing (which I haven't done recently).
\begin{code}
-- instance Read E where
-- readsPrec d = prun expression . tokens
rdexp :: String -> E
rdexp = fst . head . prun expression . tokens
\end{code}
\newpage
\section{Examples}
This section codes some naturally occurring
combinators.
\subsection{CBKIWSS'}
The combinators |C|, |B|, |K|, |I| and |W| can be encoded
as expressions in our calculus.
\begin{code}
cC, cB, cK, cI, cI', cW, c0 :: E
cC = cM :*: cE :^: cM -- M to one plus E to the E
cB = cE :*: cM :^: cM -- M to the C
cK = cE :*: c0 :^: cM -- 0 to the C
-- | cI = V"@" :^: V"0" |
cI' = cE :*: cE :^: cM -- E to the C
cW = cE :*: (cE :+: cE) :^: cM -- twice E to the cC
\end{code}
The `real-word' versions:
\begin{code}
combC = (*) * (^) ^ (*) -- |flip|, transpose.
combB = (^) * (*) ^ (*) -- |(.)|, composition. |(*) ^ combC|
combI = naughtiness ^ (<>) -- |id|. also |(^) * (^) ^ (*)|, inter alia
combK = (^) * (<>) ^ (*) -- |const|. |(<>) ^ combC|
combW = (^) * ((^) + (^)) ^ (*) -- diagonalisation. |((^) + (^)) ^ combC|
naughtiness = error "Naughty!"
\end{code}
With |W|, there are several ways to define |S|. One is by brute force: first define a linearised version |S'| with an extra argument:
\begin{spec}
S' a b c1 c2 = a c1 (b c2)
\end{spec}
Then define |S a b| (the normal S combinator) to be |W (S' a b)|.
It turns out that
\begin{spec}
S' = (*) * ((*) *)
\end{spec}
which can also be written | (*) ^ (1 + (*)) |.
After a little calculation, we get something like:
\[
(\times) \times (\times)^{(\times)} \times (\times) \times
{((\wedge) \times {((\wedge) + (\wedge))}^{(\times)})}^{(\wedge)}
\]
% [*] * [*] ^ [*] * [*] * ([^] * ([^] + [^]) ^ [*]) ^ [^]
It cannot be controversial that this expression is less than entirely gorgeous.
B{\"o}hm's theory of logarithms gives a much nicer analysis of the |S| combinator (and it's
relatives).
Despite its brutality, the combinator |S'| is not without interest:
\begin{spec}
S = S' * (*) * (W ^ (^)) -- $S' \times W^{C}$
S' = S' (*)
C = S' (^)
B = S' (^) (*) -- $(\times) ^ C$
I = S' (^) (^) -- $(\wedge) ^ C$
K = S' (^) (<>) -- $(\ZERO) ^ C$
W = S' (^) ((^) + (^)) -- $((\wedge) + (\wedge)) ^ C$
S' 1 = (*)
\end{spec}
One can define the |S'| and |S| combinators as follows:
\begin{code}
combS' :: (a -> b -> c) -> (a1 -> b) -> a -> a1 -> c
combS :: (a -> b -> c) -> (a -> b) -> a -> c
combS' = let x = (*) in x * (x ^ x)
combS = combS' * (*) * (combW ^)
\end{code}
The following expressions code the |S| and |S'| combinators
combinators.
\begin{code}
cS, cS' :: E
cS = cS' :*: cW :^: cB
cS' = cM :*: (cM :^: cM)
-- the following is an example for checking that the logarithm apparatus is working.
-- It is a variant of the |S| combinator that should evaluate in the correct way.
cSalt :: E
cSalt = blog "y" (blog "x" ( (vx :*: cPair) :+: (vy :*: cE )))
\end{code}
Try | test $ vy :^: vx :^: vb :^: va :^: cSalt |. It needs two extra variables.
\subsection{Sestoft's examples}
There is a systematic way of encoding data structures (pairs, tuples, whatnot) in the $\lambda$-calculus,
sometimes called Church-encoding.
Here are some examples in the list of predefined constants in
Sestoft's Lambda calculus reduction workbench at
http://raspi.itu.dk/cgi-bin/lamreduce?action=print+abbreviations
%http://www.dina.kvl.dk/~sestoft/lamreduce/index.html.
The first line shows the definition, the remaining lines show
the reduction to arithmetic form.
\begin{spec}
pair x y z = z x y
= y ^ x ^ z
= (x ^ z) ^ (y^)
= (z ^ (x ^)) ^ (y ^)
pair x y = (x^) * (y^)
= (y^) ^ ((x^)*)
pair x = (^) * ((x^)*)
= ((x^)*) ^ ((^)*)
= ((x ^ (^))^(*)) ^ ((^)*)
pair = (^)*(*)*((^)*)
\end{spec}
\begin{code}
cPair = cE :*: cM :*: (cE :^: cM)
\end{code}
Closely related to pairing is the Curry combinator,
which
satisfies | f^cCurry x y = f (x , y) |.
The following are alternate versions of this combinator.
\begin{code}
cCurry' = cK :*: (cPair :^: cA)
cCurry = cB :*: (cPair :^: cM)
cCurry_demo = (vz :^: (vy :^: vx :^: cPair) :^: vf) :&: (vz :^: vy :^: vx :^: vf :^: cCurry)
\end{code}
Try | test $ cK :^: cCurry_demo |, then | test $ c0 :^: cCurry_demo |.
\begin{spec}
tru x y = x
= x^y^(<>)
= (y^(<>))^(x^)
tru x = (<>)*(x^)
= (x^)^((<>)*)
tru = (^)*((<>)*)
= (<>)^C
\end{spec}
\begin{spec}
fal x y = y
= y ^ x ^ (<>)
fal = (<>)
\end{spec}
\begin{code}
cFalse = c0
cTrue = c0 :^: cC -- cK
cNot = cC
\end{code}
\begin{spec}
fst p = p tru
= tru ^ p
= p^(tru^)
fst = (tru^)
snd = (fal^)
\end{spec}
\begin{code}
cFst = cTrue :^: cE
cSnd = cFalse :^: cE
\end{code}
\begin{spec}
iszero n = n (K fal) tru
= n ((<>)*(fal^)) tru
= tru ^ ((<>)*(fal^)) ^ n
= (n^(((<>)*(fal^))^))^(tru^)
iszero = (((<>)*(fal^))^)*(tru^)
\end{spec}
\begin{code}
cIszero = cTrue :^: (cFalse :^: cK) :^: cPair
\end{code}
\subsection{Tupling, projections}
We use the usual notation $(a,b)$ for pairs.
In general
\begin{spec}
(a1,...,ak) = (a1^) * ... * (ak^)
\end{spec}
and the projection operators $\pi^k_i$ have the form
\begin{spec}
(K^i (K^j))^ where i + j + 1 = k
\end{spec}
In fact the binary projections are defined using the booleans,
and other projections are defined using
more general selector terms such as |\ x1 .. xn -> xi|.
This is done by applying | (^) | to the selector.
\begin{spec}
\ p -> p sel = (sel^)
\end{spec}
The booleans are |K = (K^0) (K^1)| and |0 = (K^1) (K^0)|.
Selecting the |i|'th element of a stack with |i+j+1| elements is |(K^i) (K^j)|.
It may be interesting to remark that
\begin{spec}
(a,a) = W pr a = (a^) * (a^) = a ^((^) + (^))
\end{spec}
So that |pr ^ W = (^) + (^) = W ^ C|
TODO: code some expressions
\subsection{Permutations}
\begin{code}
perms_abc :: [E]
perms_abc =
[ vc :^: vb :^: va -- id
, vc :^: va :^: vb -- exp (2-chain)
, vb :^: vc :^: va -- flip (2-chain)
, va :^: vc :^: vb -- bury/rotate-down (3-chain)
, vb :^: va :^: vc -- pair/rotate-up (3-chain)
, va :^: vb :^: vc -- flipped pair (2-chain)
]
inst_xyz :: E -> E
inst_xyz = (vz :^:) . (vy :^:) . (vx :^:)
bind_abc :: E -> E
bind_abc = blog "a" . blog "b" . blog "c"
c_perms :: [E] -- list of permutation combinators
c_perms = fmap (eval . bind_abc) perms_abc
see_perms = NList (fmap (eval . inst_xyz) c_perms)
\end{code}
\subsection{Fixpoint operators}
Among endless variations, two fixed-point combinators stand out, Curry's and Turing's.
Both their fixed point combinators use self application.
This of course banishes us from the realm of combinators that Haskell can type,
but what the heck. There is syntax for it. We diagonalise exponentiation.
\begin{code}
cSap :: E
cSap = cE :^: cW
\end{code}
%
We call the self application combinator |sap|.
\begin{spec}
sap x = x x = W (^) x = W 1 x
So sap = (^)^W = 1^W
\end{spec}
%Note that the expressions |(^)^W| and |1^W| do not typecheck.
We call Curry's combinator simply $Y_C$.
\begin{spec}
f^Y = sap (sap * f)
Y = (sap *) * sap
= sap ^ ((*) + 1)
\end{spec}
$Y$ can thus be seen as applying
the successor of multiplication
to the value |sap|.
\begin{code}
cY_C = cSap :^: cM :^: cSuc
\end{code}
Turing's combinator is |T ^ T| %, \ie{} |T ^ sap|
where $T x y = y (x x y)$.
\begin{spec}
T x y = y (x x y) = y (sap x y) = y ((sap^C) y x)
(T^C) y x = y ((sap^C) y x) = (y . (sap^C) y) x
(T^C) y = ((sap^C) y) * y
(T^C) = (sap^C) + 1
T = ((sap^C) + 1)^C
= sap ^ ( C * (+1) * C )
\end{spec}
$T$ can thus be seen as applying a kind of dual (with respect to the involution |C|) of the
successor operator to the value |sap|.
Some expressions for
Turing's semi-Y, and his Y.
\begin{code}
cT = cSap :^: (cC :*: cSuc :*: cC)
cY_T = cT :^: cSap
\end{code}
Be careful when evaluating these things!
\subsection{Rotation combinators}
The following linear combinator |combR| `rotates' 3 arguments.
\begin{code}
combR :: a -> (b -> a -> c) -> b -> c
combR = (^) * (((*) * ((^)*))*)
combR' = (^) * (^) * ((*)*)
\end{code}
Some such operation is often provided by the instruction
set of a `stack machine', to rotate the top three entries
on the stack. It can be seen as a natural extension of the
operation that flips (that is, rotates) the top two entries.
It can be encoded as follows:
\begin{code}
cR, cR_var :: E
cR = cC :^: cC
cR_var = (V "^") :*: (V "^") :*: (V "*") :^: (V "*") -- a variant
-- an alias for left rotation. Could call it Load? (Load par3 to top)
-- abc to cab
cL :: E
cL = cPair
-- an alias for right rotation. Could call it Store? (Store top as par3)
-- abc to bca
cR_demo = vc :^: vb :^: va :^: cR
cL_demo = vc :^: vb :^: va :^: cL
\end{code}
It has a cousin, that rotates in the other direction.
This is actually the pairing combinator.
It so happens that the |cC| combinator and the |cR| are each
definable from the other.
\begin{code}
cC' = cR :^: cR :^: cR
cR' = cC :^: cC
\end{code}
To be a little frivolous, this gives us a way of churning out
endless variants of the combinators |combR| and |flip|.
\begin{code}
flip', flip'' :: (a -> b -> c) -> b -> a -> c
flip' = flip flip (flip flip) (flip flip)
flip'' = flip' flip' (flip' flip') (flip' flip')
\end{code}
\subsection{Continuations}
The function |^| which takes |a| to |a ^| pops up everywhere when playing
with arithmetical combinators.
It provides the basic means of interchanging the positions
of variables:
| a^b = b^(a^) = b^a^(^) |.
The continuation monad has a particularly simple expression in arithmetical
terms:
\begin{code}
cm_ret = (^) -- $\eta$
cm_join = (^) ^ (*) -- $\mu$
cm_map = (*) * (*)
\end{code}
It doesn't matter what the `result type' is. Letting it be |()|,
the functor can be defined as follows.
\begin{code}
type Cont a = (a -> ()) -> ()
\end{code}
\iffalse
The action on maps is
\begin{code}
cmap_CT :: E
cmap_CT = cM :*: cM
\end{code}
The unit |return| and multiplication |join|
of this monad have simple arithmetical expressions.
\begin{spec}
return :: a -> CT a
join :: CT (CT a) -> CT a
return a b = a ^ b -- ie. |return = (^)|
f `join` s = f (return s) -- ie. |join = ((^)*)|
\end{spec}
\fi
Here's their code.
\begin{code}
cRet, cMu, cMap :: E
cRet = cE
cMu = cE :^: cM
cMap = blog "m" (blog "c" (blog "k" (vm :*: vk) :^: vc))
\end{code}
We can simply define the bind operator from join and map.
\begin{code}
cBind :: E
cBind = let arg = vm :^: vc :^: cMap in blog "m" (blog "c" (arg :^: cMu))
\end{code}
Sadly, it's not very enchanting:
\[ (\wedge) \times (\wedge) \times (\wedge) \times (\times) ^ {(\times)} \times ((\times) \times (\wedge))^{(\times)}
\]
\iffalse
The bind operator |>>=| is not quite as simple.
\begin{spec}
(m >>= f) s = m (f^C . s)
(m >>= f) = (f^C) * m
= (^) * (f*) * m
(>>=)^C f m = (^) * (f*) * m
(>>=)^C f = ((^)*) . ((f*)*)
= ((f*)*) * ((^)*)
f^((>>=)^C) = (f^(*))^(*) * (^)^(*)
f^((>>=)^C) = f^((*)*(*)) * (^)^(*)
\end{spec}
You may be interested in fancy control operators (like `abort'), and
flirtations with classical logic.
The following may reduce your cravings.
Peirce's law: | ((a->b) -> a) -> a |
is interesting because it is a formula of minimal logic.
It involves only the arrow, and not |0|.
\emph{Yet} you can prove excluded
middle |a or not a| from it, where `negation' is relativised to a generic
type $r$, as |not a = a -> r|. So when defining something,
one has unrestricted access to these two cases.
Peirce's law postulates the existence of an algebra for
a certain monad, called `the Peirce monad' by Escardo\&co.
When `true' |0| (including efq) and hence true negation is
added, to minimal logic, Peirce's law implies not just
excluded middle, but full classical logic with involutive
negation, \ie{} $\neg(\neg a) = a$.
To suppose the negation of Peirce's law leads
to an absurdity. (We don't need efq for this.)
\begin{spec}
not Peirce = not a & ((a->b)->a)
=> not a & not (a->b)
= not a & not b & a
\end{spec}
We cannot hope to prove Peirce's law, but we might expect to
prove it's transform by the continuation monad |((a -> CT b) -> CT a) -> CT a|,
in which all the arrows |a -> b| have been turned into Kleisli arrows
|a -> CT b|. Or maybe even |((a -> b) -> CT a) -> CT a|.
We can ask what such a thing would look like expressed with arithmetical
combinators.
I once made an effort to do this, and got the following result (though it
is pretty certain there are some errors here):
\iffalse
\begin{spec}
(((*) * ((^) * 0 ^ (*)) ^ (^)) ^ (*) * (^)) * ((^) + (^)) ^ (*)
\end{spec}
\fi
$$
(((\times) \times ((\wedge) \times 0^{(\times)})^{(\wedge)})^{(\times) \times (\wedge)}) \times ((\wedge) + (\wedge))^{(\times)}
$$
Well, if that's an arithmetical expression of classical logic, it's neither very enlightening or beguiling!
One can however see some additive features here, namely $(\wedge) + (\wedge)$ and $0$. I find that
reassuring.
One can ask the same questions with respect to the Peirce monad.
The monadic apparatus can be encoded as follows
\begin{code}
ct :: E -> E
ct a = a :^: cE -- unit
cb :: E -> E -> E
cb m f = cE :*: (f :^: cE) :*: m -- bind
cCTret, cCTjoin, cCTbind :: E
cCTret = cE
cCTjoin = cCTret :^: cM
cCTbind = blog "m" (blog "f" (cb (V"m") (V"f")))
\end{code}
It may be interesting to point out that
$(a,b) = a^{[\wedge]} \times b^{[\wedge]} = \eta a \times \eta b$
where $\eta$ is the unit of CT.
\fi
\subsection{Peano numerals}
Oleg Kiselyov
%\cite{oleg}
was once and may still be interested in what I think he calls or once called `p-numerals'.These
are (so to speak) related to primitive recursion as the Church
numerals are related to iteration. So the successor of n is
not
\begin{spec}
\ f,z->f(n f z)
\end{spec}
as it is with Church numerals, but rather
\begin{spec}
\ f,z->f n (n f z)
\end{spec}
I have heard other people than Oleg express an interest in this encoding. It's not un-natural.
So, letting the variable |n| vary over p-numerals, one has
\begin{spec}
n b a = b (n-1) (b (n-2) ... (b 1 (b (<>) a)) ...)
\end{spec}
Using the combinators of this paper, one can derive
\begin{spec}
n b = b (<>) * b 1 * ... * b (n-2) * b (n-1)
= b^((<>)^) * b^(1^) * ... * b^((n-2)^) * b^((n-1)^)
= b^(((<>)^) + (1^) + ... + ((n-2)^) + ((n-1)^))
\end{spec}
By exponentiality ($\zeta$),
\begin{spec}
n = ((<>)^) + (1^) + ... + ((n-2)^) + ((n-1)^)
\end{spec}
%(Remember that all the numbers here are to be understood as p-numerals!)
In fact, if |Osucc| is Oleg's successor, we have | Osucc n = n + (n^) |.
\begin{spec}
(<>)_p = (<>)
1_p = ((<>)^)
2_p = ((<>)^) + (((<>)^)^)
3_p = ((<>)^) + (((<>)^)^) + ((((<>)^) + (((<>)^)^))^)
...
\end{spec}
One may be reminded here of von-Neumann's representation for ordinals, which has $n \mapsto n \cup \{n\}$.for its successor operation,
and the empty set $\{\}$ for its origin.
\[
\newcommand{\MT}{\{\}}
\newcommand{\B}[1]{\{#1\}}
\begin{array}{rcl}
0 &=& \MT \\
1 &=& \B{\MT}\\
2 &=& \B{\MT,\B{\MT}}\\
3 &=& \B{\MT,\B{\MT},\B{\MT,\B{\MT}}}\\
&& ...
\end{array}
\]
Clearly the operation of raising to the power of exponentiation (that
takes |n| to |(n^)|) plays the role of the singleton operation $n \mapsto \{n\}$.
\begin{code}
cOsuc :: E -> E
cOsuc e = e :+: (e :^: cE)
cOzero :: E
cOzero = V"0"
cO :: Int -> E -- allows inputting numerals in decimal.
cO n = let x = cOzero : [cOsuc t | t <- x ] in x !! n
\end{code}
\subsection{sgbar, \etc{}}
|sgbar|, or exponentiation to base zero, is the function which is 1 at
0, and only at 0. On numbers, it is the characteristic
function of those that are zero.
\begin{code}
sgbar :: C b2 (a -> Endo b1) -- eg C x x where x = N b.
sgbar = ((<>) ^) -- real-world
cSgbar :: E
cSgbar = c0 :^: cE -- code
sgbar' :: Endo (N a)
sgbar' n s z = n (const z) (s z)
cSgbar' :: E
cSgbar' = let v1 = vz :^: vs
ef = vz :^: cK
in (blog "n" (blog "s" (blog "z" (v1 :^: ef :^: vn ))))
\end{code}
Using |sgbar|, we can define |sg|, which is 0
at 0, and 1 elsewhere (the sign function, or the characteristic
function of the non-zero numbers).
\begin{code}
sg :: ((a1 -> Endo b2) -> (a2 -> Endo b3) -> c) -> c
sg = sgbar * sgbar
sg' :: Endo (N a)
sg' n s z = n (const (s z)) z
cSg = cSgbar :*: cSgbar
cSg' = let v1 = vz :^: vs
ef = v1 :^: cK
in (blog "n" (blog "s" (blog "z" (vz :^: ef :^: vn ))))
\end{code}
It may be clearer to write it |sg a = (<>) ^ (<>) ^ a|. Think of double negation.
Using |sg| and |sgbar|, we can implement a form of boolean
conditionals. | IF b=0 THEN a ELSE c |
can be defined as | a*sg(b)+c*sgbar(b) |.
In fact we have forms of definition by finite cases.
%\iffalse
\section{Benedicto benedicatur}
Examples I once used, with |test|, to demo some reduction sequences.
Little thought has been given to this.
\begin{code}
demo1Add = let d = va :+: vb in vx :^: d
demo1Zero = let d = V"0" in vx :^: d
demo1Mul = let d = va :*: vb in vx :^: d
demo1One = let d = V"1" in vx :^: d
-- show that the logarithm of an exponential behaves as expected
demoExp = let d = (va :^: cPair) :*: (vb :^: cE)
in vx :^: d
demoExp' = let d = (va :*: cPair) :+: (vb :*: cE)
in vy :^: vx :^: d
-- two equivalent codings
demoAdd = let c = (va :^: cE) :+: (vb :^: cE)
d = cPair :*: cM :*: c :^: cE -- curry c
in vz :^: vy :^: vx :^: d
demoAdd' = let c = (va :^: cE) :+: (vb :^: cE)
d = cPair :+: c :^: cK -- curry c
in vz :^: vy :^: vx :^: d
demoNaught = let d = c0 :*: c0 :^: cE in d
\end{code}
One can think of addition as repetition of the successor operation,
as mutiplication as repetition of addition to zero,
and of exponentiation as repetition of mutiplication to one.
The successor operation can be defined as |(1 +)| or |(+ 1)|.
\begin{code}
demoSuc = c1 :^: cA
demoSuc' = c1 :^: cA :^: cC
demoPlus = demoSuc :^: cPair
demoTimes = demoPlus :*: (c0 :^: cPair :^: cC)
demoPower = demoTimes :*: (c1 :^: cPair :^: cC)
demoPlus' = demoSuc' :^: cPair
demoTimes' = demoPlus' :*: (c0 :^: cPair :^: cC)
demoPower' = demoTimes' :*: (c1 :^: cPair :^: cC)
\end{code}
You can for example ask ghci to evaluate | test $ demoAdd' |.
%\fi
\end{document}
Safe place for debris:
Don't use code environment!
*Main> let l = V"*" :*: cB :*: (V"+" :^: V"*") ; r = V"*" :+: (V"+" :^: cK) :+: (V"*" :*: V"*") in test (vc :^: vb :^: va :^: l)
let sb = (vc :^: vb) :^: vc :^: va ; s = blog "a" (blog "b" (blog "c" sb)) ; k = blog "a" (blog "b" va) in test $ vw :^: vz :^: vy :^: vx :^: s
let b = vz :^: vy :^: vx ;
p0 = blog "z" . blog "y" . blog "x" ; -- converse pair = cPair :^: cC swap(a,c)
p1 = blog "z" . blog "x" . blog "y" ; -- rotation = cR = cC :^: cC
p2 = blog "y" . blog "x" . blog "z" ; -- exponential = cE swap(a,b)
p3 = blog "y" . blog "z" . blog "x" ; -- pair = cPair = cE :*: cC
p4 = blog "x" . blog "y" . blog "z" ; -- identity = c1 = cC :*: cC
p5 = blog "x" . blog "z" . blog "y" ; -- flip = cC swap(b,c)
p = (p0 b :&: p1 b :&: p2 b :&: p3 b :&: p4 b :&: p5 b) in test $p
let t = cE :*: cC ; vec h = vc :^: vb :^: va :^: h in test $ vx :^: (vec t :&: vec cPair)
\iffalse
test $ vx :^: ((va :^: cPair) :*: (vb :^: cE))
--demonstrates that a ^ b = a ^ cPair :*: b ^ cE
-- demonstrates log-like behaviour of _^K.
test $ inst_xyz $ (va :^: (cK :*: cE) :+: vb :^: (cK :*: cE)) :^: cCurry -- (va :+: vb) :^: cK
-- demonstrates (+ b) as iteration of (+1).
let suc = c1 :^: cA :^: cC ; plus b = (suc :^: cPair) :*: (b :^: cE) in test $ vy :^: vx :^: plus c3
-- a definition of addition as iterated successor
let suc = c1 :^: cA :^: cC ; t = (cE :*: (suc :^: cPair) :^: cM) :^: cC in test $ c3 :^: c0 :^: t
-- t is a redefinition of the addition combinator
let suc = c1 :^: cA :^: cC ; t = (cE :*: (suc :^: cPair) :^: cM) :^: cC in test $ vy :^: vx :^: (cA :*: (c1 :^: cE)) -- [+]*(1^)
let m = (cSuc :^: cE) :*: (c0 :^: cPair :^: cC) ; e = (m :^: cC) :*: (c1 :^: cPair :^: cC) in test $ vz :^: vs :^: c3 :^: c2 :^: e
let a = cSuc :^: cE ; m = (cSuc :^: cE) :*: (c0 :^: cPair :^: cC) ; e = (m :^: cC) :*: (c1 :^: cPair :^: cC) in test $ vs :^: c3 :^: c2 :^: e
\fi