In this lecture, we will look at the decomposition of the arrow type (i.e. intuitionistic implication) in terms of unary exponentiation and logarithm, and show some applications of it.

We will start by recalling the notion of type isomorphism, reviewing the meta-theoretic facts that hold of it in presence of disjoint union types.

We shall then show that it makes sense to use the transformation aᵇ=exp(b·log(a)) in the context of types by defining a normal form for the type language {→,×,+} and applying it to obtain a simplification of the standard axioms of η-equality for the {→,×,+}-typed λ-calculus.

We shall end by hinting at proof theoretic applications. In particular, we shall show how to extend the type normal form to the first-order quantifiers and define a constructive arithmetical hierarchy of formulas resembling the classical arithmetical hierarchy.

http://hal.inria.fr/hal-00991147

http://arxiv.org/abs/1502.04634

http://arxiv.org/abs/1601.04876