Go backward to Categorical Product Go up to Top

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₁. (IV1)(IV2)
• Theorem does not hold for eager semantics!
  • (lambdaX:comm. lambdaY:comm. Y)loop
  • "Weak exponentiation"