<p>You can use <a href="http://en.wikipedia.org/wiki/Attribute_grammar" rel="nofollow">attribute grammars</a>. They give a formal framework for describing transformation of trees but are also in practical use, e.g. in ANTLR where you can define compiler from trees to trees (or code) using tree grammars .</p>

CC BY-SA 3.0
2011-05-28T08:46:55.970Z
2011-05-28T08:46:55.970Z
Raphael
<p>Look at Bob Harper's <a href="http://www.cs.cmu.edu/~rwh/plbook/book.pdf">book</a>. It provides loads of declarative formalisms for specifying programming language semantics and so forth. Chapter 6 describes declaratively how to translate concrete into abstract syntax. You could use the same ideas to translate one language into another.</p>

<p>Following Harper (and many others), you could write rules defined inductively on the structure of your source syntax, as follows:</p>

<p>$\begin{array}{c}
a \leadsto e \qquad b \leadsto f \qquad x=foo(a,b,e,f) \\
\hline
\mathsf{K}~a~b \leadsto \mathsf{S}~e~f~x
\end{array}
$</p>

<p>Here $\mathsf{K}$ is a constructor in your source language and $\mathsf{S}$ is in your target language. $foo$ is some function which may compute other required information (it too could be defined as a set of rules).
The translation function/relation essentially inductively decomposes your source syntax and produces a term in your target. You can also thread through additional information to help with the translation process. For example, your rule could look like:</p>

<p>$\begin{array}{c}
E&#39;\vdash a \leadsto e \qquad E&#39;&#39;\vdash b \leadsto f \qquad x=foo(E,E&#39;,E&#39;&#39;,a,b,e,f) \qquad E&#39; = \cdots
\qquad E&#39;&#39;=\cdots \\
\hline
E\vdash \mathsf{K}~a~b \leadsto \mathsf{S}~e~f~x
\end{array}
$</p>

<p>Here $E$ can store any information that needs to be threaded through.</p>

<p>Note that such specifications differ very little from a standard recursive function defined inductively in the program syntax. But they may be easier to read, and they may actually define a relation, rather than a function, by allowing a little nondeterminism.</p>

CC BY-SA 4.0
2018-08-23T11:28:59.657Z
book's link is dead, try instead http://www.cs.cmu.edu/~rwh/isml/book.pdf
Badr Bellaj
CC BY-SA 3.0
2011-05-26T08:21:16.647Z
2011-05-26T08:43:28.260Z
2011-05-26T08:43:28.260Z
Dave Clarke
<p>I'm looking for a declarative formalism to describe the transformation of an abstract syntax tree generated by the parsing of one formal language into second formal language. An example of a transformation that it would have to describe is to transform following,</p>

<pre><code>type Bool : Type {
    value false : Bool;
    value true : Bool;
};
</code></pre>

<p>into the following,</p>

<p>$Bool : Type;$</p>

<p>$Bool = (Unit \lor Unit);$</p>

<p>$true : Bool;$</p>

<p>$true = (inj_0 unit);$</p>

<p>$false : Bool;$</p>

<p>$false = (inj_1 unit);$</p>

<p>The only thing I can think of is defining piecewise-defined recursive function with nodes of the abstract syntax tree of the original language as input. Is there not a more concise way of declaring the transformation?</p>

<p>I've already implemented such transformations straightforwardly and compositionally in the programming language <em>Haskell</em> but I'm not doing so well on formalising the tranformation.</p>

<p>Also, to be clear I am <em>not</em> talking about attaching semantic actions t the original grammar (or an attribute grammar) because I assume an abstract syntax tree has already been generated by parsing the first formal language because other analysis and rewriting needs to be done on such a tree.</p>

<p>Note that I have no interest in algorithmic efficiency of such a formalism, I only want to show that a injective function from the original formal language to the second formal language exists.</p>

<p>I know I must have read about this in the formal language literature but I can't think of anything specific. I've probably forgotten something really obvious...</p>

<h3>Edit:</h3>

<p>What about natural deduction style? How could such translations be represented in natural deduction? I'll have to think about that...</p>

CC BY-SA 3.0
2011-05-24T16:49:05.933Z
How more direct can you get than a function from one language to another? This should be a fairly straightforward and clean task if you are not interested in efficiency.
Christopher Monsanto
CC BY-SA 3.0
2011-05-26T13:15:17.167Z
Why must the function be injective?
Dave Clarke
<fl.formal-languages><pl.programming-languages>
What formalisms exist to describe the translation of an abstract syntax tree into another formal language?
Anthony
# What formalisms exist to describe the translation of an abstract syntax tree into another formal language?

(Asked by: username_0 on 2011-05-24)

I'm looking for a declarative formalism to describe the transformation of an abstract syntax tree generated by the parsing of one formal language into second formal language. An example of a transformation that it would have to describe is to transform following,
type Bool : Type {
    value false : Bool;
    value true : Bool;
};

into the following,
$Bool : Type;$
$Bool = (Unit \lor Unit);$
$true : Bool;$
$true = (inj_0 unit);$
$false : Bool;$
$false = (inj_1 unit);$
The only thing I can think of is defining piecewise-defined recursive function with nodes of the abstract syntax tree of the original language as input. Is there not a more concise way of declaring the transformation?
I've already implemented such transformations straightforwardly and compositionally in the programming language Haskell but I'm not doing so well on formalising the tranformation.
Also, to be clear I am not talking about attaching semantic actions t the original grammar (or an attribute grammar) because I assume an abstract syntax tree has already been generated by parsing the first formal language because other analysis and rewriting needs to be done on such a tree.
Note that I have no interest in algorithmic efficiency of such a formalism, I only want to show that a injective function from the original formal language to the second formal language exists.
I know I must have read about this in the formal language literature but I can't think of anything specific. I've probably forgotten something really obvious...
Edit:
What about natural deduction style? How could such translations be represented in natural deduction? I'll have to think about that...

**Tags:** fl.formal-languages, pl.programming-languages

> **Comments:**
> **username_1**: How more direct can you get than a function from one language to another? This should be a fairly straightforward and clean task if you are not interested in efficiency.  
> **username_2**: Why must the function be injective?  

---

## 2 answers

### Answer by username_2 on 2011-05-26. Score: 6 | Accepted answer

Look at Bob Harper's [book](http://www.cs.cmu.edu/~rwh/plbook/book.pdf). It provides loads of declarative formalisms for specifying programming language semantics and so forth. Chapter 6 describes declaratively how to translate concrete into abstract syntax. You could use the same ideas to translate one language into another.

Following Harper (and many others), you could write rules defined inductively on the structure of your source syntax, as follows:

$\begin{array}{c}
a \leadsto e \qquad b \leadsto f \qquad x=foo(a,b,e,f) \\
\hline
\mathsf{K}~a~b \leadsto \mathsf{S}~e~f~x
\end{array}
$

Here $\mathsf{K}$ is a constructor in your source language and $\mathsf{S}$ is in your target language. $foo$ is some function which may compute other required information (it too could be defined as a set of rules).
The translation function/relation essentially inductively decomposes your source syntax and produces a term in your target. You can also thread through additional information to help with the translation process. For example, your rule could look like:

$\begin{array}{c}
E'\vdash a \leadsto e \qquad E''\vdash b \leadsto f \qquad x=foo(E,E',E'',a,b,e,f) \qquad E' = \cdots
\qquad E''=\cdots \\
\hline
E\vdash \mathsf{K}~a~b \leadsto \mathsf{S}~e~f~x
\end{array}
$

Here $E$ can store any information that needs to be threaded through.

Note that such specifications differ very little from a standard recursive function defined inductively in the program syntax. But they may be easier to read, and they may actually define a relation, rather than a function, by allowing a little nondeterminism.

> **Comments:**
> **username_4**: book's link is dead, try instead http://www.cs.cmu.edu/~rwh/isml/book.pdf  

---

### Answer by username_3 on 2011-05-28. Score: 3

You can use [attribute grammars](http://en.wikipedia.org/wiki/Attribute_grammar). They give a formal framework for describing transformation of trees but are also in practical use, e.g. in ANTLR where you can define compiler from trees to trees (or code) using tree grammars .


---

