Home
|
Introduction
A genoid theory is a
category (A, G) of two objects such that
G together with two morphisms x:
G -> A and
+: G ->
G
is the product of A and G, and
G is a dense object. A left algebra of
(A, G) is a functor from
(A, G) to the category Set
of sets preserving the product.
| Let A =
hom(G, A) and G =
hom(G, G). For any pair (a, u) in
A X G let [a,
u]: G -> G be the
unique morphism such that x[a, u] =
a and + [a, u] = u. Then u
= [xu, +u] for any u in
G. |
A clone theory is a category
(A, G) of two objects such that
G together with an infinite sequence of morphisms
x1, x2, .. from G to
A is a countable power of
A. A left algebra of
(A, G) is a functor from
(A, G) to Set preserving the
power. Left algebras of clone theories are main objects of study in
universal algebra.
| Let A =
hom(G, A) and G =
hom(G, G). For any infinte
sequence a1, a2, .... in
A let [a1, a2...]:
G ->
G be the unique morphism
such that xi[a1,
a2...] = ai. Then u =
[x1u, x2u,...] for any
u in G. Any clone theory determines a
genoid theory with x = x1, + = [
x2, x3 ,
...]. |
Let (A, G) be a genoid.
Let P be a right act of the monoid G =
hom(G, G). An abstract binding
(resp. cobinding) operation on P is a
map σ: P
-> P such that (σp)u =
σ(p[x, u+]) (resp. σ(pu) =
(σp)[x, u+]) for any p in P and
u in G. A binding algebra of
(A, G) is a right
act P of G equipped with some binding, cobinding
operations, and other homomorphism of right acts
Pn ->
P for various arity n
≥ 0. Here are two
important types of binding algebras:
| Lambda
Calculus: A reflexive lambda calculus is
a genoid (A, G) together with a
binding operation λ: A ->
A and a cobinding operation λ*: A
-> A such that
λλ* = idA. An extensive lambda
calculus is a genoid (A,
G) together with a bijective binding operation
λ: A -> A.
First Order Logic: A quantifier
algebra with terms in a genoid
(A, G) is a right act P of
G with an abstract binding operation : P -> P and two
homomorphisms F:
P0 ->
P, and =>: P
X P
-> P such that
(i) P is a Boolean
algebra with respect to the derived operations (V, Λ, ~, F,
T).
(ii) ∃ (p ∨ q) =
(∃ p) ∨ (∃ q) for
any p,q, in P.
(iii) p <
(∃p)+ for any p in P.
| |
|
Genoids |
A genoid (A,
G, x, +, [ ]) consisting of a
monoid (G, e), a right act A of G, an
element x of A, an element + of G, and a map
[ ]: A X
G -> G such that
for any a in A and u in G we
have
(i) x[a, u] =
a.
(ii) +[a, u] =
u.
(iii) u = [xu,
+u].
In the following we fix a
genoid, denoted simply by (A, G). We shall write
[a1, a2, ..an, u]
for [a1, [a2, [...
[an, u]...]]]. |
|
Let x1 = x, xi
=
xi+ for any i
> 0. Then (iii) extends to
u = = [x1u,
x2u, ... xnu, +nu]
for any n > 0. Let κn: G
-> An be the
map sending each u to the expression [x1u,
x2u, ... xnu]. We assume y, z, w, ...in
{x1, x2 ,
x3 ...}, which are called syntactical
variables. |
| Let P be a right act of the
monoid G. We say an element p of P has a
finite rank n > 0 if pu = pv for any u,
v in G with κn(u) = κn(v). We say
p has a finite rank 0 (or p is closed) if pu
= pv for any u, v in G. An element of P is
called finitary if it has a finite rank. We say P (or
A) is locally finitary if any of its element is
finitary. We say an element p of P is
independent of xn if p
= p[x1, .. x(n-1),
x(n+1),
+n]. |
|
Let
δ: G -> G be the map sending u to [x, u+]. Then
δ is an endomorphism of monoid G. Let - = [x, e],
where e is the unit of G. Then (δ, +, -) is a
monad on G (viewed as a one-object category). Thus G
is a Kleisli algebra. |
| If P is
any right act of G denote by PA the
new right act (P, *) of G defined by
p*u = p(δu) = p[x,
u+]. A map σ: P -> P is an abstract
binding (resp. cobinding)
operation if it is a homomorphism from PA to P (resp. from P to PA). Such abstract binding operations can be applied to defined
algebraic theories for lambda calculus and first order logic. The
traditional binding operation σxi : P -> P (for each
variable xi) is then defined as the derived
operation:
σxi.p = σ(p[x2, x3, ...,
xi, x1, +i+1]).
If y = xi
then σy.p means
σxi.p. |
| The main difference between an
abstract binding σ: P -> P and a derived operation
σy: P
->
P is that
σ reduces the rank n > 0
of a finitary element of P by 1 while σy
makes any element of P independent of the variable
y (i.e. binding y). Hence if p has a finite
rank n > 0 then σnp and σx1. ...
σxn.p are
always closed. |
| If P is
a right act of G let ev: PA
X
A
-> P
be the map defined by ev(p, a) =
p[a, e]. For any right act T of
G define Λ: hom(T X A, P) ->
hom(T, PA) given by
(Λf)t = f(t+, x).
Define Λ-1:
hom(T, PA) ->
hom(T X A, P) by
(Λ-1g)(t, a) = g(t)[a,
e] = ev(g(t), a).
It is easy to see that
Λ is the inverse of Λ-1. Hence Λ is
bijective. Thus (PA, ev) is the exponent in
the the cartesian closed category ActG of right
acts of G. |
| Letting
T = P = A we obtain a bijection Λ:
hom(A X A, A)->
hom(A, AA). This is the starting point of lambda
calculus. |
| We say (A, G) is an extensive
genoid (or (extensive) lambda
calculs) if it has a bijective abstract binding operation λ:
A ->
A. Denote by λ*
the inverse of λ. Then λ* is a cobinding operation.
Thus λ* determines a homomorphism
Λ-1(λ*): A X A -> A defined by
ab = λ*a[b, e].
Hence a genoid is extensive iff there is a
homomorphism A X
A -> A of right acts of G such that the induced
cobinding operation λ* defined by
λ*(a) = (a+)x
is bijective. Since idA
= λ*λ = λλ*, we have the following
two axioms
| a =
(λa)+x |
(or a = (λy.a)y for any
y) |
(β-conversion) |
| a =
λ(a+x) |
(or a
= λy.(ay) if a is independent of
y) |
(η-conversion) |
|
| We list some of
the useful properties for lambda calculus: (a, b, c in
A and u in G)
(1) (λa)b
= a[b, e].
(2) ((λ
a)u)b = a[b,
u].
(3) (λa+)b = a.
(4) (λn a)+n
xn...x1 = a for any integer n
> 0.
(5) If a has a finite rank n
> 0 then (λna)xn...x1
= a and λna is closed.
Thus
(λna)an...a1
= (λna)xn...x1
[a1, ..., an, e] =
a[a1, ..., an]
(6) An element
a has a finite rank n > 0 if and only if
there is a closed element c such that
a =
cxn...x1. |
|
The following closed terms play important
role in lambda calculus (notation:
λy1...yn.a =
λy1.(λy2.(..(λyn.a)...)).)
I =
λy,y = λx1.
K =
λyz.y = λλ x2
S =
λyzw.yw(zw) =
λλλx3x1(x2
x1).
It follows from
(5) we have
Ia
= x1 [a, e] = a.
Kab =
x2[b, a, e] =
a.
Sabc =
(x3x1(x2x1))[c,
b, a, e] = ac(bc). |
| |
|
Clones |
A clone is a set
A such that
(i) The set A* of
all the infinite sequences [a1, a2,
...] of elements of A is a monoid with a unit
[x1, x2, ...].
(ii) A is a right act of A*.
(iii) xi[a1,
a2, ...] = ai for any
[a1, a2, ...] and i >
0. |
| Any clone A determines a
genoid (A, A*, x1, +, [ ])
with + = [x2, x3, ...] and
[a1, [b1, b2 ,..]] =
[a1, b1, b2 ,..].
Conversely, assume (A, G) is a any genoid. Denote by
F(A) the set of finitary elements of A. For any
a in F(A) with a finite rank n >
0 and [a1, a2, ...] in
F(A)* define a[a1, a2,
...] = a[a1, a2, ...,
an , e], which is independent of the choice
of n. Let
[a1, a2,
...][b1, b2, ...] =
[a1[b1, b2, ...],
a2[b1, b2, ...],
...]
Then F(A)* is a monoid with
the unit [x1, x2, ...],
F(A) is a right act of A*, and
xi[a1, a2, ...] =
ai. Thus (F(A),
F(A)*) is a locally finitary genoid. If A =
F(A) is locally finitary then we have a canonical
homomorphism of genoids (A, G) -> (A, A*) sending each
u in G to [x1u, x2u, ...
xnu, ...]. Since any abstract binding operation
preserving finitary elements, if (A, G) is a lambda
calculus, then so is (F(A),
F(A)*). |
| The class of
genoids forms a variety of 2-sorted heterogeneous finitary algebras
with universes A and G. The class of clones
forms a variety of infinitary algebras with universe
A. |
Let N be a full
subcategory of a category X. A Kleisli
triple over N is a system T =
(T, η,
*-) consisting
of functions
(a) T: Ob N -> Ob X,
(b) η assigns to each object A in
N a morphism ηA: A
-> TA,
(c) *-
maps each morphism f: B -> TC with B, C in
N to a morphism *f: TB -> TC, such that for
any g: C -> TD with D
in N
(i) *f*g = *(f*g
).
(ii) ηB*f =
f.
(iii) *ηC =
idTC. |
| If N = X
we obtain the original definition for a Kleisli triple over a
category, which is an alternative description of a
monad. |
Let N be a
full subcategory of a category X. A
clone over N is a pair (K,
T) where K is a category and T is a functor
T: K -> X such that
for any A, B, C in N
(i). Ob N =
Ob K.
(ii). K(A, B) =
X(A, TB).
(iii). f(Tg) = fg for
any f in K(A, B) and g in K(B,
C). |
| The notions of a clone over N
is equivalent to a Kleisli triple over N
defined above.. |
Examples: Let X = Set be the category of sets.
1. A clone over a singleton is equivalent to a
monoid.
2. A clone over a finite set is equivalent to a
unitary Menger algebra.
3. A clone over a countable set
is equivalent to a clone defined above.
4. A clone over
the subcategory {0, 1, 2, ...} of finite sets is
equivalent to a clone in the classical sense (or a Lawvere theory).
5. A clone over a one-object category is equivalent to a Kleisli
algebra. |
| 1. Clone Theory, its
Syntax and Semantics, and Applications to Lambda Calculus and
Algebraic Logic |
|
pdf |
| 2. Clones and Genoids
(Basic Concepts) |
html |
pdf |
| 3. Clones and Genoids in
Lambda Calculus and First Order Logic |
|
pdf |
| |
|
| |
