S is injective
Recall the definition of S:
S : (A -> B -> C) -> (A -> B) -> A -> C
S = λ x y a -> x a (y a)
I am assuming a simple semantics of sets and functions, and by S being injective I mean that S x = S x' ⇒ x = x', which can be trivially shown below:
S x = S x'
≡ { η expansion, for all y : A -> B, a : A }
(∀ a, y : S x y a = S x' y a)
≡ { definition of S }
(∀ a, y : x a (y a) = x' a (y a))
⇒ { choose y = K b for some b }
(∀ a, b : x a (K b a) = x' a (K b a))
≡ { definition of K: K b a = b }
(∀ a, b : x a b = x' a b)
≡ { pointwise equality }
x = x'
Now that we know S is injective, there ought to exist some function S⁻¹ such that S⁻¹ ○ S = id. Nakano san claimed that a definition would be:
S⁻¹ : ((A -> B) -> A -> C) -> A -> B -> C
S⁻¹ = λ x a b -> x (K b) a
That S⁻¹ ○ S = id is easy to see:
S⁻¹ (S x) a b
= (S x) (K b) a
= x a (K b a)
= x a b
From another direction, we have only S ○ S⁻¹ ⊆ id since S is not a surjective function. How the range of S look like? Inspecting the definition of S. Since y is applied only once to a, the value of y on other input does not matter. That is, the range of S consists of only functions e such that:
e y a = e y' a for all y, y' such that y a = y' a ......(1)
We will show that S (S⁻¹ e) = e for all e satisfying (1):
S (S⁻¹ e) y a
= { definition of S }
S⁻¹ e a (y a)
= { definition of S⁻¹ }
e (K (y a)) a
= { by (1), since K (y a) a = y a }
e y a
Inverting higher-order functions?
Some endnotes. Once Nakano and I thought we discovered how to invert higher-order functions (and even derive the necessary side conditions, like the one on e above) by drawing λ expressions as trees and manipulating them. It turned out that I overlooked something obvious in the very beginning and the result was a disaster.
