diff options
Diffstat (limited to 'main.org')
| -rw-r--r-- | main.org | 11 |
1 files changed, 9 insertions, 2 deletions
@@ -4,6 +4,7 @@ #+context_header_extra: \environment env #+options: syntax:vim toc:nil #+property: header-args:coq :noweb no-export :padline yes :tangle Main.v +#+auto_tangle: t One main optimisation in compilers targeting parallel architectures is /instruction scheduling/, where instructions are placed into time-slots statically so that these can be executed in parallel. @@ -90,8 +91,8 @@ with expression_list : Type := The interesting thing to note about this abstract expression type is that it is weakly typed, meaning predicates are not any different to standard expressions. The correctness is therefore governed by how the expressions are generated, and to what resource they are assigned to in the -final expression tree. We will also need some kind of equality check for these expressions, so we -can assume that we can implement a decidable check like the following: +final expression tree.[fn:2] We will also need some kind of equality check for these expressions, so +we can assume that we can implement a decidable check like the following: #+begin_src coq Axiom expression_dec: @@ -122,6 +123,8 @@ Definition predicated A := NE.non_empty (pred_op * A). Definition pred_expr := predicated expression. #+end_src +We can then also speak about equivalence between two predicates by + #+begin_src coq Definition apred : Type := expression. Definition apred_op := @Predicate.pred_op apred. @@ -240,5 +243,9 @@ End R_indexed. * Footnotes +[fn:2] We can see that predicates are actually not needed in the semantics of any other +expressions. It might therefore be better to create a separate ~predicate_expression~ which will +only set predicates based on a condition. + [fn:1] This post uses noweb syntax to specify pieces of code defined elsewhere, and will link to those pieces of code directly. |