transitive closure is written . The following typing rules are also common to all systems in the cube:The difference between the systems is in the pairs of sorts that are allowed in the following two typing rules: The correspondence between the systems and the pairs allowed in the rules is the following: Each direction of the cube corresponds to one pair (excluding the pair shared by all systems), and in turn each pair corresponds to one possibility of dependency between terms and types: allows terms to depend on terms. allows types to depend on terms. allows terms to depend on types. allows types to depend on types. Comparison between the systems λ→ A typical derivation that can be obtained isor with the arrow shortcutclosely resembling the identity (of type ) of the usual λ→. Note that all types used must appear in the context, because the only derivation that can be done in an empty context is . The computing power is quite weak, it corresponds to the extended polynomials (polynomials together with a conditional operator). λ2 In λ2, such terms can be obtained aswith . If one reads as a universal quantification, via the Curry-Howard isomorphism, this can be seen as a proof of the principle of explosion. In general, λ2 adds the possibility to have impredicative types such as , that is terms quantifying over all types including themselves.The polymorphism also allows the construction of functions that were not constructible in λ→. More precisely, the functions definable in λ2 are those provably total in second-order Peano arithmetic. In particular, all primitive recursive functions are definable. λP In λP, the ability to have types depending on terms means one can express logical predicates. For instance, the following is derivable:which corresponds, via the Curry-Howard isomorphism, to a proof of .From the computational point of view, however, having dependent types does not enhance computational power, only the possibility to express more precise type properties. The conversion rule is strongly needed when dealing with dependent types, because it allows to perform computation on the terms in the type. For instance, if you have and , you need to apply the conversion rule to obtain to be able to type . λω In λω, the following operatoris definable, that is . The derivationcan be obtained already in λ2, however the polymorphic can only be defined if the rule is also present. From a