Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Get rid of yet another fixme.

4 left.
  • Loading branch information...
commit f0a5c49852f56518fcadfda276f0e24768b951d1 1 parent bb580af
Jesper Louis Andersen authored
Showing with 11 additions and 5 deletions.
  1. +11 −5 report/janus1.tex
16 report/janus1.tex
View
@@ -295,11 +295,17 @@ \section{Determinism properties of \januso{}}
commutative rule when we want to rewrite $x +_{32} y$ into $y +_{32}
x$.
-\fixme{This section needs to be rewritten}
-However, the formalization in \coq{} is slightly different to work
-around a problem with mutually defined theorems. This means we cannot
-utilize the theorem in further development as it is given in the
-development.
+In \coq{} we need mutually defined theorems in order to define
+backwards and forwards determinism at the same time. \coq{} version
+8.2 has this feature in a more user friendly way than earlier
+versions, where you had to manually refine a fixpoint. Unfortunately,
+we failed to get it to define the correct induction hypothesis.
+
+The workaround we use is to define forwards determinism under the
+assumption of backwards determinism and vice versa. Hence, we can't
+use the theorems in further developments, but it allows us to use
+backwards determinism in the case for \texttt{uncall}.
+
\begin{thm}
\label{thm:j1-fwd-det}
\januso{} is forward deterministic, ie:
Please sign in to comment.
Something went wrong with that request. Please try again.