Go backward to Categorical Product
Go up to Top
Go forward to References
Categorical Exponentiation
- Categorical exponentiation theta theta
- apply<(lambdaI:theta. E),
U> = with I=U do E
- (lambdaI:theta. apply<E, I>)
= E, if pi |- E: theta
theta
- Theorem:
- For the lazy evaluation semantics, theta
theta := theta theta is the
categorical
exponentiation.
- apply = lambdaI: (theta
theta)xtheta. (I1)(I2)
- Theorem does not hold for eager semantics!
- (lambdaX:comm. lambdaY:comm. Y)loop
- "Weak exponentiation"
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: records.tex,v 1.1 1996/05/20 12:33:10 schreine Exp schreine