Go backward to
Model of the Programming Language
Go up to
Top
Go forward to
Categorical Exponentiation
Categorical Product
Categorical product
theta
1
x
theta
2
<E
1
, E
2
>
V
1 = E
1
<E
1
, E
2
>
V
2 = E
2
<E
V
1, E
2
V
2>= E, if
pi
|- E:
theta
1
x
theta
2
Theorem:
For the lazy evaluation semantics,
theta
1
x
theta
2
:= {
fst
:
theta
1
,
snd
:
theta
2
} is the categorical product.
Theorem does
not
hold for eager semantics!
<
bottom
, E>=
bottom
"Tensor product"
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998
