Go backward to Model of the Programming Language
Go up to Top
Go forward to Categorical Exponentiation
Categorical Product
- Categorical product theta x theta
- <E, E>1 = E
- <E, E>2 = E
- <E1, E2>= E,
if pi |- E: theta x theta
- Theorem:
- For the lazy evaluation semantics,
theta x theta := {fst:theta,
snd:theta} is the categorical product.
- Theorem does not hold for eager semantics!
- <bottom, E>= bottom
- "Tensor product"
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: records.tex,v 1.1 1996/05/20 12:33:10 schreine Exp schreine