% -*- LaTeX -*-
% $Id: Subst.lhs,v 1.7 2002/12/20 13:12:51 lux Exp $
%
% Copyright (c) 2002, Wolfgang Lux
% See LICENSE for the full license.
%
\nwfilename{Subst.lhs}
\section{Substitutions}
The module {\tt Subst} implements substitutions. A substitution
$\sigma = \left\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\right\}$ is a
finite mapping from (finitely many) variables $x_1,\dots,x_n$ to
some kind of expression or term.
In order to implement substitutions efficiently composed
substitutions are marked with a boolean flag (see below).
\begin{verbatim}
> module Subst where
> import qualified Data.Map as Map
> data Subst a b = Subst Bool (Map.Map a b) deriving Show
> idSubst :: Ord a => Subst a b
> idSubst = Subst False Map.empty
> substToList :: Ord v => Subst v e -> [(v,e)]
> substToList (Subst _ sigma) = Map.toList sigma
> bindSubst :: Ord v => v -> e -> Subst v e -> Subst v e
> bindSubst v e (Subst comp sigma) = Subst comp (Map.insert v e sigma)
> unbindSubst :: Ord v => v -> Subst v e -> Subst v e
> unbindSubst v (Subst comp sigma) = Subst comp (Map.delete v sigma)
\end{verbatim}
For any substitution we have the following definitions:
\begin{displaymath}
\begin{array}{l}
\sigma(x) = \left\{\begin{array}{ll}
t_i&\mbox{if $x=x_i$}\\
x&\mbox{otherwise}\end{array}\right. \\
\mathop{{\mathcal D}om}(\sigma) = \left\{x_1,\dots,x_n\right\} \\
\mathop{{\mathcal C}odom}(\sigma) = \left\{t_1,\dots,t_n\right\}
\end{array}
\end{displaymath}
Note that obviously the set of variables must be a subset of the set
of expressions. Also it is usually possible to extend the substitution
to a homomorphism on the codomain of the substitution. This is
captured by the following class declaration:
\begin{verbatim}
class Ord v => Subst v e where
var :: v -> e
subst :: Subst v e -> e -> e
\end{verbatim}
With the help of the injection \texttt{var}, we can then compute the
substitution for a variable $\sigma(v)$ and also the composition of
two substitutions
$(\sigma_1 \circ \sigma_2)(e) \mathop{:=} \sigma_1(\sigma_2(e))$. A
naive implementation of the composition were
\begin{verbatim}
compose sigma sigma' =
foldr (uncurry bindSubst) sigma (substToList (fmap (subst sigma) sigma'))
\end{verbatim}
However, such an implementation is very inefficient because the
number of substiutions applied to a variable increases in
$\mathcal{O}(n)$ of the number of compositions.
A more efficient implementation is to apply \texttt{subst} again to
the value substituted for a variable in
$\mathop{{\mathcal D}om}(\sigma)$. However, this is correct only as
long as the result of the substitution does not include any variables
which are in $\mathop{{\mathcal D}om}(\sigma)$. For instance, it is
impossible to implement simple variable renamings in this way.
Therefore we use the simple strategy to apply \texttt{subst} again
only in case of a substitution which was returned from \texttt{compose}.
\begin{verbatim}
substVar :: Subst v e => Subst v e -> v -> e
substVar (Subst comp sigma) v = maybe (var v) subst' (Map.lookup v sigma)
where subst' = if comp then subst (Subst comp sigma) else id
> compose :: (Show v,Ord v,Show e) => Subst v e -> Subst v e -> Subst v e
> compose sigma sigma' =
> composed (foldr (uncurry bindSubst) sigma' (substToList sigma))
> where dom = domain sigma
> dom' = domain sigma'
> domain = map fst . substToList
> composed (Subst _ sigma) = Subst True sigma
\end{verbatim}
Unfortunately Haskell does not (yet) support multi-parameter type
classes. For that reason we have to define a separate class for each
kind of variable type for these functions. We implement
\texttt{substVar} as a function that takes the class functions as an
additional parameters. As an example for the use of this function the
module includes a class \texttt{IntSubst} for substitution whose
domain are integer numbers.
\begin{verbatim}
> substVar' :: Ord v => (v -> e) -> (Subst v e -> e -> e)
> -> Subst v e -> v -> e
> substVar' var subst (Subst comp sigma) v =
> maybe (var v) subst' (Map.lookup v sigma)
> where subst' = if comp then subst (Subst comp sigma) else id
> class IntSubst e where
> ivar :: Int -> e
> isubst :: Subst Int e -> e -> e
> isubstVar :: IntSubst e => Subst Int e -> Int -> e
> isubstVar = substVar' ivar isubst
\end{verbatim}
The function \texttt{restrictSubstTo} implements the restriction of a
substitution to a given subset of its domain.
\begin{verbatim}
> restrictSubstTo :: Ord v => [v] -> Subst v e -> Subst v e
> restrictSubstTo vs (Subst comp sigma) =
> foldr (uncurry bindSubst) (Subst comp Map.empty)
> (filter ((`elem` vs) . fst) (Map.toList sigma))
\end{verbatim}