title: How to apply single β-step at the root
body: <p>I got the following task:</p>
  <blockquote>
  <p>Let type Strat = Term -&gt; [Term] be the type of reduction strategies.
  Implement the strategy root :: Strat which applies a single β-step at
  the root (if possible)</p>
  </blockquote>
  <p>Now I know how the different strategies (applicative order reduction, normal order reduction, ...) work.</p>
  <p>My question now is, now: Every time I apply a β-step to a term, i get another term. Why should i return a list of terms?</p>
  <p>What I have till now is:</p>
  <pre><code>type Id = String
  data Term =     Var Id              -- Var ... variable
                  | App Term Term     -- App ... application
                  | Abs Id Term       -- Abs ... abstraction
                  deriving(Show)
  
  root :: Term -&gt; Term
  root (Var v)            = Var v             -- var
  root (Abs x s)          = Abs x s           -- abs
  root (App (Abs x t) u)  = subst x u t       -- root
  root (App s u) = App (root s) (root u)      -- app-l and app-r
  
  -- where subst x s t computes t[x := s], satisfying the freshness constraint.
  subst :: String -&gt; Term -&gt; Term -&gt; Term
  ...(already implemented)
  </code></pre>
  <p><strong>EDIT:</strong>
  Maybe I should mention the next two steps, that have to be made, to make the question clear:</p>
  <blockquote>
  <p>Implement a strategy combinator nested :: Strat -&gt; Strat that, given a
  strategy s, results in a new strategy which tries to apply s at all
  non-root positions.</p>
  <p>Building on the previous functions, implement single-step call by name reduction cbn :: Strat.</p>
  </blockquote>