Yes, it is always possible. Here's one particularly simple algorithm:
[[\x -> x]] ~> id
[[\x -> e]] ~> const e -- when x does not appear in e
[[\x -> e1 e2]] ~> [[\x -> e1]] <*> [[\x -> e2]]
For example, here's how that might look for eliminating z
from your expression.
\x y -> [[\z -> (x + y) * z]]
~> \x y -> [[\z -> (*) (x + y)]] <*> [[\z -> z]]
~> \x y -> const ((*) (x + y)) <*> id
We can then go again, this time eliminating y
.
\x -> [[\y -> const ((*) (x + y)) <*> id]]
~> \x -> [[\y -> (<*>) (const ((*) (x + y)))]] <*> [[\y -> id]]
~> \x -> ([[\y -> (<*>)]] <*> [[\y -> const ((*) (x + y))]] ) <*> const id
~> \x -> (const (<*>) <*> ([[\y -> const]] <*> [[\y -> (*) (x + y)]] )) <*> const id
~> \x -> (const (<*>) <*> (const const <*> ([[\y -> (*)]] <*> [[\y -> x + y]] ))) <*> const id
~> \x -> (const (<*>) <*> (const const <*> (const (*) <*> ([[\y -> (+) x]] <*> [[\y -> y]])))) <*> const id
~> \x -> (const (<*>) <*> (const const <*> (const (*) <*> (const ((+) x) <*> id )))) <*> const id
We could go again, to eliminate x
, but this is already messy enough. The point is that this can all be done purely mechanically, without requiring insight from the person (or machine) doing the point free translation.
For fun, here's the final form if you follow this algorithm:
const (<*>) <*> (const ((<*>) (const (<*>))) <*> (const ((<*>) (const const)) <*> (const ((<*>) (const (*))) <*> (const (<*>) <*> (const const <*> (const (+) <*> id)) <*> const id)))) <*> const (const id)
It's obvious that this algorithm is geared towards simplicity over readability of the result!
Full listing for the code to generate that answer:
{-# LANGUAGE LambdaCase #-}
type Var = String
data Term
= S | K | I
| Variable Var
| Lambda Var Term
| App Term Term
deriving (Eq, Ord, Read, Show)
free :: Var -> Term -> Bool
free v = \case
Variable v' -> v == v'
Lambda v' t -> v /= v' && free v t
App t t' -> free v t || free v t'
_ -> False
translate :: Term -> Term
translate = \case
Lambda v t -> case t of
_ | not (free v t) -> App K t
Variable{} -> I
App e1 e2 -> App (App S (translate (Lambda v e1))) (translate (Lambda v e2))
Lambda{} -> translate (Lambda v (translate t))
_ -> error "The impossible happened: variable is not free, but term is not a variable, app, or lambda"
App t t' -> App (translate t) (translate t')
t -> t
doThing :: Term
doThing = Lambda "x" . Lambda "y" . Lambda "z" $
App
(App
(Variable "(*)")
(App
(App (Variable "(+)") (Variable "x"))
(Variable "y")
)
)
(Variable "z")
pp :: Term -> String
pp = \case
S -> "(<*>)"
K -> "const"
I -> "id"
Variable v -> v
Lambda v t -> "\\" ++ v ++ " -> " ++ pp t
App (App S t) t' -> ""
++ case t of
Lambda{} -> "(" ++ pp t ++ ")"
_ -> pp t
++ " <*> "
++ case t' of
App (App S _) _ -> "(" ++ pp t' ++ ")"
_ -> pp t'
App t t' -> ""
++ case t of
Lambda{} -> "(" ++ pp t ++ ")"
_ -> pp t
++ " "
++ case t' of
App{} -> "(" ++ pp t' ++ ")"
_ -> pp t'