Go backward to Categorical ProductGo up to Top |

- Categorical exponentiation
`theta`_{1}*=>*`theta`_{2}`apply`<(`lambda`I:`theta`. E), U> =_{1}`with`I=U`do`E- (
`lambda`I:`theta`._{1}`apply`<E, I>) = E, if`pi`|- E:`theta`_{1}*=>*`theta`_{2}

- Theorem:
- For the lazy evaluation semantics,
`theta`_{1}*=>*`theta`:=_{2}`theta`_{1}*->*`theta`is the categorical exponentiation._{2} `apply`=`lambda`I: (`theta`_{1}*=>*`theta`)x_{2}`theta`. (I_{1}*V*1)(I*V*2)

- For the lazy evaluation semantics,
- Theorem does
*not*hold for eager semantics!- (
`lambda`X:`comm`.`lambda`Y:`comm`. Y)`loop` - "Weak exponentiation"

- (

Author: Wolfgang Schreiner

Last Modification: May 14, 1998