By chance, I came upon a blog entry by Masahiro Sakai (酒井政裕) in which he, after reading my short comment on my previous homepage “Do you know that the `S`

combinator is injective? I have a simple algebraic proof!”, tried to construct the inverse of `S`

and showed that `S⁻¹ ○ S = id`

in, guess what, Agda!

Wow, people were actually reading what I wrote! This made me feel that I have to be a bit more responsible and, at least, provide the proof when I claim I have one. So, here it is.

### 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'
```

I would usually leave out the `∀`

‘s in derivations, but in this case, they are explicitly written to emphasise that `b`

is indeed universally quantified.

### So, what is the inverse of S?

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.

Does anyone know of some related work on inverting higher order functions? The only one I know is Samson Abramsky’s paper A Structural Approach to Reversible Computation, but I am not sure whether it is about reversibility/invertibility in the same sense.

Pingback: -= Linkage 2007.12.13 =-

ShinLoren S, thanks for pointing that out!

Loren SAs a general matter, a left inverse of a (necessarily injective) function is always also a right inverse on the range of the function. That is, if

`g f = Id`

, then`f g(t) = f g f(s) = f(s) = t`

for`t = f(s)`

in the range of`f`

. This makes your demonstration just before “Inverting higher order functions” unnecessary.Charles StewartI’ve posted this observation as a story on LtU.

Shinlf,

Yes, I know about Djinn! In fact when I thought I found a general way to invert functions, I was merely constructing a term having the right type. After my talk, one of the audience fired up Djinn and showed me how it can be done. It must be one of my worst talks..

Frank Atanassow,

Oh, I’ve probably omitted too many steps. The reasoning goes like this:

Chris Rathman,

Thanks! I will have a read. The team I used to work with was also working on bidirectionality and I have to read that paper anyway…

Chris RathmanOff hand, Benjamin Pierce’s work on Bijection and Bidirectional programming come to mind. See: http://lambda-the-ultimate.org/node/1526

Frank AtanassowIn your first proof, it looks to me like b should be existentially quantified. Why do you say it is universally quantified?

lfTry Djinn! Passing it the type of S^-1:

f ? ((a->b) -> (a->c)) -> (a -> b -> c)

it gives you

f a b c = a (\ _ -> c) b

right away :-)