Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p>It's probably impossible without violating the ‘legitimacy’ of HOAS, in the sense that the <code>E =&gt; E</code> must be used not just for binding in the object language, but for computation in the meta language. That said, here's a solution in Haskell. It abuses a <code>Literal</code> node to drop in a unique ID for later substitution. Enjoy!</p> <pre><code>import Control.Monad.State -- HOAS representation data Expr = Lam (Expr -&gt; Expr) | App Expr Expr | Lit Integer -- Rotate transformation rot :: Expr -&gt; Expr rot e = case e of Lam f -&gt; descend uniqueID (f (Lit uniqueID)) _ -&gt; e where uniqueID = 1 + maxLit e descend :: Integer -&gt; Expr -&gt; Expr descend i (Lam f) = Lam $ descend i . f descend i e = Lam $ \a -&gt; replace i a e replace :: Integer -&gt; Expr -&gt; Expr -&gt; Expr replace i e (Lam f) = Lam $ replace i e . f replace i e (App e1 e2) = App (replace i e e1) (replace i e e2) replace i e (Lit j) | i == j = e | otherwise = Lit j maxLit :: Expr -&gt; Integer maxLit e = execState (maxLit' e) (-2) where maxLit' (Lam f) = maxLit' (f (Lit 0)) maxLit' (App e1 e2) = maxLit' e1 &gt;&gt; maxLit' e2 maxLit' (Lit i) = get &gt;&gt;= \k -&gt; when (i &gt; k) (put i) -- Output toStr :: Integer -&gt; Expr -&gt; State Integer String toStr k e = toStr' e where toStr' (Lit i) | i &gt;= k = return $ 'x':show i -- variable | otherwise = return $ show i -- literal toStr' (App e1 e2) = do s1 &lt;- toStr' e1 s2 &lt;- toStr' e2 return $ "(" ++ s1 ++ " " ++ s2 ++ ")" toStr' (Lam f) = do i &lt;- get modify (+ 1) s &lt;- toStr' (f (Lit i)) return $ "\\x" ++ show i ++ " " ++ s instance Show Expr where show e = evalState (toStr m e) m where m = 2 + maxLit e -- Examples ex2, ex3, ex4 :: Expr ex2 = Lam(\a -&gt; Lam(\b -&gt; App a (App b (Lit 3)))) ex3 = Lam(\a -&gt; Lam(\b -&gt; Lam(\c -&gt; App a (App b c)))) ex4 = Lam(\a -&gt; Lam(\b -&gt; Lam(\c -&gt; Lam(\d -&gt; App (App a b) (App c d))))) check :: Expr -&gt; IO () check e = putStrLn(show e ++ " ===&gt; \n" ++ show (rot e) ++ "\n") main = check ex2 &gt;&gt; check ex3 &gt;&gt; check ex4 </code></pre> <p>with the following result:</p> <pre><code>\x5 \x6 (x5 (x6 3)) ===&gt; \x5 \x6 (x6 (x5 3)) \x2 \x3 \x4 (x2 (x3 x4)) ===&gt; \x2 \x3 \x4 (x4 (x2 x3)) \x2 \x3 \x4 \x5 ((x2 x3) (x4 x5)) ===&gt; \x2 \x3 \x4 \x5 ((x5 x2) (x3 x4)) </code></pre> <p>(Don't be fooled by the similar-looking variable names. This is the rotation you seek, modulo alpha-conversion.)</p>
    singulars
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. VO
      singulars
      1. This table or related slice is empty.
    2. VO
      singulars
      1. This table or related slice is empty.
    3. VO
      singulars
      1. This table or related slice is empty.
 

Querying!

 
Guidance

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload