Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sav08:set_constraints_for_algebraic_datatype_inference [2008/05/22 00:13]
vkuncak created
sav08:set_constraints_for_algebraic_datatype_inference [2015/04/21 17:30] (current)
Line 5: Line 5:
 **Example** **Example**
  
- Using the following grammar :+Consider data type definition 
   type form = Atom of string   type form = Atom of string
-            | And of form*form +            | And of form * form 
-            | Or of form*form+            | Or of form * form
             | Not of form             | Not of form
  
- we can have the following types : $= \lbrace AtomAnd(\_ ​\_)Or(\_ , \_), Not \_ \rbracewhich is an infinite set ("​_"​ represents any kind of type).+We represent values of this data type as ground terms in language ​$= \{ atom,not,and,or\}$. 
 + 
 +Define function:
  
-But if we define the following function : 
   let rec elimOr(f : form) : form =   let rec elimOr(f : form) : form =
       match f with       match f with
Line 21: Line 23:
    S4: | Not(f1) -> Not(elimOr f1)    S4: | Not(f1) -> Not(elimOr f1)
  
-It is clear that the output types of this function ​is a subset ​of $F$ (as the $Or$ is removed)In fact, if we define $res$ as the resulting type of this function, $res$ can be computed ​by computing ​the fixpoint ​of : $S_1 \cup S_2 \cup S_3 \cup S_4 \subseteq res$ +We infer the subset ​of formulas returned by this function ​using set constraints. ​ Introduce set for each case of pattern matching expression Let 'res' denote ​the set of values that can be returned ​by the function. ​ We obtain the system ​of constraints: 
- +\begin{equation*} 
-  - $Atom \subseteq S_1$ +\begin{array}{l} 
-  - $And(res, res) \subseteq S_2$ +   atom \subseteq S_1 \\ 
-  - $Not(And(Not(res), ​Not(res))) \subseteq S_3$ +   and(res, res) \subseteq S_2 \\ 
-  - $Not(res) \subseteq S_4$ +   not(and(not(res), ​not(res))) \subseteq S_3 \\ 
- +   not(res) \subseteq S_4 \\  
-In this particular case, the fixpoint is : $Atom \cup And(res, res) \cup Not(res) ​\subseteq res$ which computes correctly the fact that the $Or$ has been removed. +   res = S_1 \cup S_2 \cup S_3 \cup S_4 
 +\end{array} 
 +\end{equation*}
  
 +We can prove that the least fixpoint is the same as the least fixpoint of
 +\begin{equation*}
 +    res = atom \cup and(res,​res) \cup not(res)
 +\end{equation*}
 +the last expression is a description of the solution set.  We can use it later on to prove that the result does not mention '​or'​ syntax tree node.
  
   * [[http://​theory.stanford.edu/​~aiken/​publications/​papers/​fpca93.ps|Type inference]]. ​ Semantics of untyped lambda calculus.   * [[http://​theory.stanford.edu/​~aiken/​publications/​papers/​fpca93.ps|Type inference]]. ​ Semantics of untyped lambda calculus.
   * [[http://​theory.stanford.edu/​~aiken/​publications/​papers/​popl94.ps|Soft typing with conditional types]]   * [[http://​theory.stanford.edu/​~aiken/​publications/​papers/​popl94.ps|Soft typing with conditional types]]
 +  * [[http://​lara.epfl.ch/​dokuwiki/​doku.php?​id=projects:​matcheck|Verifying Pattern Matching in Scala]]
  
 
sav08/set_constraints_for_algebraic_datatype_inference.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice