Skip to content

Overview

Jump to bottom
yunjeong-lee edited this page Jan 11, 2023 · 4 revisions

Framework Overview

In this document, we explain how tree automata are used to remove ambiguities -- in the form of shift/reduce conflicts -- from CFG of a small language called myLang (containing +, * operations and conditional IF-THEN-ELSE).

Our major contributions can be summarized as follows:

  • Formalized synthesis algorithm:
    • Examples provided by the user are treated as specificatoins.
    • Angluin's framework is further developed to learn tree automata.
    • Through interactions with the user, tree automata are synthesized according to this Angluin's framework.
  • Automated grammar disambiguation:
    • We automate the process of grammar disambiguation based on formal properties of intersection of tree automata.
  • Application of the idea for more complicated language:
    • We demonstrate the applicatoin of ideas for more complicated language that resemble the real programming languages.

Step 1. CFG $G$ for myLang

Given that a language has ambiguities in the form of shift/reduce conflicts, the first step involves constructing a CFG $G$ for the language. $G$ is defined as a tuple $(V, \Sigma, S, P)$ where

  • $V$ is a set of non-terminals (aka variables),
  • $\Sigma$ is a set of terminals,
  • $S$ is a set of start symbols, and
  • $P$ is a set of productions.

CFG $G$ of myLang is defined with the following tuple:

G  := (V, Σ, S, P)

V   = { E, C }
Σ   = { N, B, +, *, (, ), IF, THEN, ELSE }
S   = { E }
P   = { C       -> B                    ;
        E       -> N                    ;
        E       -> B                    ;
        E       -> E + E                ;
        E       -> E * E                ;
        E       -> ( E )                ;
        E       -> IF C THEN E          ;
        E       -> IF C THEN E ELSE E   }

The grammar $G$ is specified in the parser.mly:

  • $V$ refers to exp and cond_exp,
  • $\Sigma$ refers to %token excluding EOF (i.e., INT, TRUE, FALSE, PLUS, MUL, LPAREN, RPAREN, IF, THEN, and ELSE),
  • $S$ is exp, and
  • $P$ is described by the lines below.
(* parser.mly *)
%start program
%%

program : expr EOF { $1 };

cond_expr:
  | TRUE { Bool true }
  | FALSE { Bool false }
  ;

expr:
  | INT  { Int $1 }
  | expr PLUS expr { Plus ($1, $3) }
  | expr MUL expr { Mul ($1, $3) }
  | LPAREN expr RPAREN { Paren $2 }
  | IF cond_expr THEN expr { If ($2, Then ($4, Else Na)) }
  | IF cond_expr THEN expr ELSE expr { If ($2, Then ($4, Else $6)) }
  ;

In our implementation, Converter.mly_to_cfg extracts relevant lines -- i.e., the above lines -- from the parser.mly and coverts to its corresponding CFG. Running the project with the above grammar results in the shift/reduce conflicts:

$ dune exec ./main.exe
Warning: 4 states have shift/reduce conflicts.
Warning: 9 shift/reduce conflicts were arbitrarily resolved.

Step 2. Mapping CFG $G$ to TA $A$

Before dealing with the conflicts in Step 3, we first convert the CFG $G$ to its corresponding TA $A$ by mapping the components of $G$ to those of $A$ (largely labeling the productions).

$A$ is defined as a tuple $(Q, F, S, \Delta)$ where

  • $Q$ is a set of states,
  • $F$ is a set of (ranked) constructor labels (aka alphabet),
  • $S$ is a set of root states, and
  • $\Delta$ is a set of productions.

Note that this is a top-down automata where the $A$ accepts a tree $t$ if it starts from a root state in $S$ and expanding downward can construct the tree $t$.

$Q$ (set of states) corresponds to $V$ (set of non-terminals) of $G$, added with ϵ. $F$ (alphabet) is defined based on the $\Sigma$ (set of terminals) of $G$, where each of its arity is computed based on the number of exprs in respective production rule. $S$ (set of root states) refers to the first expr that appears in the productions. For our toy language, initial TA $A$ is defined with the following tuple:

A  := (Q, F, S, Δ)

Q   = { E, ϵ }
F   = { <+, 2>, <*, 2>, <(), 1>, <N, 1>, <B, 1>, <IF1, 2>, <IF2, 3>, <ϵ, 1> }
S   = { E }
Δ   = { E ->_N ϵ        ;
        E ->_B ϵ        ;
        E ->_+ E E      ;
        E ->_* E E      ;
        E ->_() E       ;
        E ->_IF1 E E    ;
        E ->_IF2 E E E  }

Step 3. Generate examples based on conflict(s) in the language

In the process of designing a language, ambiguities in the grammar are identified and warned by the parser generator. In case of myLang, the Menhir parser generator provides explanations about conflicts in the parser.conflicts file. Note that the file is located in the _build/default/ directory upon compilation. If there are no conflicts in the grammar, no parser.conflicts file will be generated upon compilation.

For the grammar $G$, following lines in parser.conflicts are used to generate examples.

** Conflict (shift/reduce) in state 12
** Tokens involved: PLUS MUL
⋮
expr MUL expr
         expr . PLUS expr
⋮

** Conflict (shift/reduce) in state 10
** Tokens involved: PLUS MUL
⋮
expr PLUS expr
          expr . PLUS expr
⋮

** Conflict (shift/reduce) in state 14
** Tokens involved: PLUS MUL
⋮
IF expr THEN expr ELSE expr 
                            expr . PLUS expr 
⋮

** Conflict (shift/reduce) in state 8
** Tokens involved: PLUS MUL ELSE
⋮
IF expr THEN expr 
                  expr . PLUS expr 
⋮

That is to say, 9 shift/reduce conflicts refer to conflicts from the following expressions (which we call Example ##):

  1. expr MUL expr PLUS expr
  2. expr PLUS expr MUL expr
  3. expr PLUS expr PLUS expr
  4. expr MUL expr MUL expr
  5. IF expr THEN expr ELSE expr PLUS expr
  6. IF expr THEN expr ELSE expr MUL expr
  7. IF expr THEN expr PLUS expr
  8. IF expr THEN expr MUL expr
  9. IF expr THEN IF expr THEN expr ELSE expri

Here, we assume that an ambiguity reported by Menhir is represented with the most concise expression that covers other bigger, complicated expressions containing the same type of ambiguity.

Examples

Based on the Example 01, we can create following options for the user:

(* Example 01 *)

     (Option 1)         |      (Option 2)       
                        |                       
        MUL             |         PLUS          
       /   \            |         /  \          
     expr PLUS          |       MUL  expr       
          /  \          |      /  \             
       expr  expr       |    expr expr

That is, the $G$ contains ambiguities caused by precedence involving + and *. When there is expr * expr + expr, it is not sure whether to do perform expr * expr first or expr + expr first. Without specifying precedence, Menhir arbitrarily resolves this conflict, presumably resulting in an incorrect computation of expr * (expr + expr). For example, 2 * 3 + 4 is evaluated as Mul(2,Plus(3, 4)).

Similarly, following options are generated for subseqeuent expressions:

(* Example 02 *)

     (Option 1)         |      (Option 2)       
                        |                       
        PLUS            |          MUL          
       /   \            |         /  \          
     expr  MUL          |      PLUS  expr       
          /  \          |      /  \             
       expr  expr       |    expr expr

This example is similar to Example 01 above, except that MUL and PLUS are swapped.

(* Example 03 *)

     (Option 1)         |      (Option 2)       
                        |                       
        PLUS            |         PLUS          
        /  \            |         /  \          
     expr PLUS          |       PLUS expr       
          /  \          |       /  \             
       expr  expr       |     expr expr

This refers to the associativity of + operator. When there is $n_1 + n_2 + n_3$, it is not sure whether to do perform $n_1 + n_2$ first or $n_2 + n_3$ first. As in the earlier example, Menhir arbitrarily resolves this conflict, with the right associativity of $n_1 + (n_2 + n_3)$.

(* Example 04 *)

     (Option 1)         |      (Option 2)       
                        |                       
         MUL            |          MUL          
        /  \            |         /  \          
     expr  MUL          |        MUL expr       
          /  \          |       /  \             
       expr  expr       |     expr expr

This example is similar to Example 03 above, except that it involes MUL instead of PLUS.

(* Example 05 *)

             (Option 1)                     |              (Option 2)       
                                            |                       
                PLUS                        |                  IF      
               /    \                       |               /  |  \         
              IF     expr                   |           cexpr expr PLUS      
            /  |  \                         |                      /  \             
        cexpr expr expr                     |                    expr expr
                                            |
  (IF cexpr THEN expr ELSE expr) PLUS expr  |     IF cexpr THEN expr ELSE (expr PLUS expr)

This example is similar to Example 03 above, except that it involes MUL instead of PLUS.

Step 4. The user selects an example

In this step, we let the user --- aka the language designer --- select one example based on their preference. Note that there are two different formats to present examples to the user: trees and code snippets. The format will be finalized based on the user study in the future. In this document, we're using the tree format as shown in the Step 3 above.

For simplicity, suppose that we are only dealing with the first example and the Option 2 was selected by the user to eliminate the conflicts.

Step 5. TA $A'$ encoding restrictions

This example (Option 2) is subsequently fed to the following algorithm to automatically generate a TA $A'$ encodinig restrictions.

$$ a + b $$

(TODO: Here, we need to further clarify an algorithm involved in generating $A'$ based on the example selected by the user.)

(TODO: Take note of Angluin's Algorithm and apply it in Tree languages context. Explain how the algorithm I came up with is principled.)

Now we specify a TA $A'$ encoding restrictions as follows:

A' := (Q', F, S', Δ')

Q'  = { X, Y, ϵ }
F   = { <+, 2>, <*, 2>, <(), 1>, <N, 1>, <ϵ, 1> }
S'  = { X }
Δ'  = { X ->_+ X X  ;
        X ->_ϵ Y    ;

        Y ->_N ϵ    ;
        Y ->_* Y Y  ;
        Y ->_() X   }

TRE that corresponds to the above TA is written as follows:

TRE : 
    ( ( +([],[]) )* . ( *([],[]) )* . ( N() | ()([]) ) )*

Step 6. TA $A''$ resulted from intersection of $A$ and $A'$

TA $A''$ resulted from taking intersection of $A$ and $A'$ (i.e., $A \cap A'$ where $A = (Q, F, S, \Delta)$ and $A' = (Q', F, S', \Delta')$) is defined as a tuple $(Q'', F, S'', \Delta'')$ where:

  • $Q''$ is a cross product of $Q$ and $Q'$, i.e., $Q \times Q'$,
  • $S''$ is a cross product of $S$ and $S'$, i.e., $S \times S'$, and
  • $\Delta''$ is a cross product of $\Delta$ and $\Delta'$, i.e., $\Delta \times \Delta'$.

Based on the above definition of intersection, we can define $A''$ as follows:

A'':= (Q'', F, S'', Δ'')

Q'' = { EX, EY, ϵ }
F   = { <+, 2>, <*, 2>, <(), 1>, <N, 1>, <ϵ, 1> }
S'' = { EX }
Δ'' = { EX ->_N ϵ       ;
        EX ->_+ EX EX   ;
        EX ->_* EY EY   ;
        EX ->_() EX     ;
        EY ->_N ϵ       ;
        EY ->_* EY EY   ;
        EY ->_() EX     }

By introducing epsilon introductions, the productions $\Delta''$ can be simplified further, as shown below:

Δ'' = { EX ->_+ EX EX   ;
        EX ->_ϵ EY      ;
        EY ->_* EY EY   ;
        EY ->_N ϵ       ;
        EY ->_() EX     }

Step 7. Convert TA $A''$ to CFG $G'$

The resulted $A''$ is converted back to CFG $G'$ by unlabeling the productions:

G' := (V', Σ', S', P')

V'  = { X, Y }
Σ'  = { N, +, *, (, ) }
S'  = { X }
P'  = { X -> X + X  ;
        X -> Y      ;
        Y -> Y * Y  ;
        Y -> N
        Y -> ( X )  }

(TODO: mention how this CFG gets converted to a new .mly file)

(TODO: include further example to illustrate a situation where there are multiple conflicts - e.g., dangling else, etc.)

References

[1]: Adams, M. D., & Might, M. (2017). Restricting grammars with tree automata. Proceedings of the ACM on Programming Languages, 1(OOPSLA), 1-25. https://doi.org/10.1145/3133906.

Footnotes

i: This dangling-else example is not obvious from the parser.conflicts file. Presumably, this has to do with how Menhir -- a LR(1) parser generator -- identifies shift/reduce conflicts.

Clone this wiki locally