Fast - guide

FAST: Functional Abstraction of Symbolic Transducers

This tutorial demonstrates some basic features of Fast.

Fast is a programming language for expressing tree to tree transformers and for analyzing various properties of those transformers. We introduce the Fast through some simple examples

TreeMap

In this first example we show how we can use Fast to model simple tree manipulating programs. Next we can use fast to answer simple questions about such programs. The following Fast program models a tree-map operation that navigates over a tree of real numbers and multiplies by 2.0 the entry of each node.

Functions

We start by defining a function that given a real number r returns 2*r. load in editor

Fun twice (x:real) : real := (* 2.0 x) 
In order to preserve the analysis, these auxiliary functions cannot be recursive.

Alphabets

The keyword Alphabet allows to define the type of our trees. BTReal defines the type of binary trees over reals. Each node of type BTReal will contain an attribute r:real and will of be built using one of the constructors B or Z. Nodes built with with the constructor B will have 2 children (both of type BTReal), while nodes built using the constructor Z will have no children. load in editor

Alphabet BTReal[r:real]{Z(0),B(2)}

Transformations

The keyword Trans allows to define tree transformations (i.e. functions from trees to trees). map_twice defines the map function we described before. Rules allow to pattern match on tree constructors. A rule B(x,y) to (B [(twice r)] (p x) (p x)) has the following meaning. Given a tree t with root B(x,y), output the tree (B [r1] t1 t2) where

load in editor
Public Trans map_twice : BTReal -> BTReal {
     B(x,y) to (B [(twice r)] (map_twice x) (map_twice y))	 
   | Z() to (Z [(twice r)])
}
Note: even though in this example the transformation map_twice only does recursion on itself, transformations in Fast can call other transformations on their right hand side

Trees

The keyword Tree allows to define trees. In this case t_2 is the result of applying map_twice to t_1. The primitive Print allows us to print the final result. load in editor

//A simple tree, and the result of applying the transformation map_twice to such tree
Tree t_1 : BTReal := (B [1.5] (Z [1.2]) (Z [1.4]))    
//Result of applying the transformation map_twice to t_1
Tree t_2 : BTReal := (apply map_twice t_1)
//Pick a tree from the domain of map_twice
Tree t_3 : BTReal := (get_witness (domain map_twice))
Note: Fast does not allow to print tree expressions due to typing requirements. If you want ot pring a tree expression store it as Tree name : A := tree_expr and then print it using Print name.

Languages

In Fast Languages (i.e. sets of trees) are first class objects. With a syntax similar to that of transformations we can define the languages geq_0 of trees containing only nodes with value greater or equal than 0, and its complement co_geq_0 in which at least one node has a negative value. Let's consider the rule B(x,y) where (>= r 0.0) given (geq_0 x) (geq_0 y) in geq_0. The rule reads as follows: given a tree t of type BTReal

The where and given clauses can also be used for transformations with the same semantics. load in editor
Public Lang geq_0 : BTReal {
     Z() where (>= r 0.0)
   | B(x,y) where (>= r 0.0) given (geq_0 x) (geq_0 y)
} 
Def co_geq_0 : BTReal := (complement geq_0) 
Notice that in the language co_geq_0 the rules are not mutually exclusive. In Fast the semantics of rules is nondeterministic, and if multiple rule applies, they are all considered in deciding whether a tree belongs to the language. The same consideration is for transformations; however in this case, if multiple rules apply for a single input, the transformation may produce multpile outputs.

Analysis

Last we show how we can use Fast to perform a simple analysis of the program we just wrote. Fast offers primitives that allow to combine transformations and languages to build more complex transformations and languages. In this eample we use the primitives restrict_inp, restrict_out, domain, and eq_lang.

  1. First we compute (restrict_out map_twice co_geq_0). This new transfromation is the same as map_twice, but it is only defined on those input for which map_twice produces outputs in the language co_geq_0.
  2. Similarly (restrict_inp map_twice_rout geq_0) is the same as map_twice_rout, but it is only defined on those input in the language geq_0.
  3. Last we check whether the transformation map_twice_rinp_rout is defined on some input using the is_empty_trans function. We will have that map_twice_rinp_rout is defined only on those trees that are in geq_0, and on which map_twice produces an output in co_geq_0. Not surprisingly, there is no such tree, and Fast is able to detect it.
load in editor
//Restrict map_twice to only output trees in co_geq_0
//If the output contains one negative number, so does the input
Def map_twice_rout1 : BTReal -> BTReal := (restrict_out map_twice co_geq_0)
Def dom_map_twice_rout1 : BTReal := (domain map_twice_rout1)
//Check domain is co_geq_0
AssertTrue (eq_lang dom_map_twice_rout1 co_geq_0)
//This times we do the same thing for positive numbers, by using the constructor
// pre_image that gives us all the inputs the produce outputs in geq_0
Def dom_map_twice_rout2 : BTReal := (pre_image map_twice geq_0)
//Positive numbers produce positive numbers
AssertTrue (eq_lang dom_map_twice_rout2 geq_0)

Code Generation

Finally, we can generate the C# program corresponding to our Fast code. load in editor

Print (gen_csharp)

Deforestation and Analysis of Programs over Trees

Deforestation is the art of trasforming a sequence of functions f1...fn into a single equivalent function f. Particularly, while to execute the sequence f1...fn on a given input, we need to produce n-1 intermediate outputs, this won't be the case for our single pass function f.

List Manipulating Programs

Consider the following two functions over lists of integers. load in editor
//Increments all the elements of the list by 1
Public Trans map_inc : IntList -> IntList {
	   nil() to (nil [0])
   | cons(x) to (cons [(inc i)] (map_inc x))
}
//Removes all the odd elements from the list
Public Trans filter_ev : IntList -> IntList {
	   nil() to (nil [0])
   | cons(x) where (odd i) to (filter_ev x)
   | cons(x) where (even i) to (cons [i] (filter_ev x))
}
In functional programming it is often common to combine similar functions in order to perform a given task. For example one might want to increment all the elements of the list, and then filter out such elements base on some criteria.

Composition in Fast

Even though in this case computing the corresponding composed function is not too hard, Fast is able to do it for us. When using the compose operator over two Fast transformation, we generate a single Fast transformation able to compute the composed function load in editor
//Compose the two functions into a single one
Def map_filt : IntList -> IntList := (compose map_inc filter_ev)
The next example shows a more complex nesting. You can load it in the editor to see the corresponding single-pass Fast program. load in editor
//Compose the four functions into a single one
Def map_filt_2 : IntList -> IntList := (compose (compose map_inc filter_ev) (compose map_inc filter_ev))

Analysis of Composed Programs

It turns out that the transformation map_filt_2 always returns the empty list. This can be checked in Fast!! In fact, if we restrict map_filt_2 to only output non-empty lists, we will get the empty transformation. load in editor
//Empty list languiage
Public Lang not_emp_list : IntList {
    nil()
}
//Non-Empty list languiage
Public Lang not_emp_list : IntList {
    cons(x)
}
//Check whether map_filt_2 ever outputs a non-empty list
Def map_filt_2_rest : IntList -> IntList := (restrict_out map_filt_2 not_emp_list)
AssertTrue (is_empty_trans map_filt_2_rest)

Type-checking

Alternatively we can use the typechecking operator, that given a transformation t and two languages input, output checks whether t maps every tree in input to a tree in output. load in editor
//Compose the four functions into a single one
Def map_filt_2 : IntList -> IntList := (compose (compose map_inc filter_ev) (compose map_inc filter_ev))
//All-lists language
Lang all_list : IntList { nil() | cons(x) }
//Non-Empty list languiage
Lang empty_list : IntList { nil() }
//Check whether map_filt_2 always outputs the empty list
AssertTrue (typecheck all_list map_filt_2 empty_list)

Finding bugs

In this example we show how the typechecking can be used to find bugs in programs. In this example we omit the last filter from the composition, and now the composed function can output a non-empty list, so the type-checking fails, and gives a counterexample. load in editor
//Compose the four functions into a single one
Def map_filt_buggy : IntList -> IntList := (compose (compose map_inc filter_ev) map_inc)
//All-list languiage
Lang all_list : IntList { nil() | cons(x) }
//Non-Empty list languiage
Lang empty_list : IntList { nil() }
//Check whether map_filt_2 always outputs the empty list
AssertTrue (typecheck all_list map_filt_buggy empty_list)
We considered programs over lists, but the same analysis can be done for tree manipulating programs
Contact Us| Privacy & Cookies | Terms of Use | Trademarks| © 2019 Microsoft