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 |
| |
|
|
|