Skip to content

Commit

Permalink
Ispell the intro.
Browse files Browse the repository at this point in the history
  • Loading branch information
jlouis committed May 18, 2009
1 parent bcbadbb commit 313b2e4
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 5 deletions.
8 changes: 4 additions & 4 deletions report/intro.tex
Expand Up @@ -12,7 +12,7 @@ \chapter{Introduction}
interesting property that programs can be run backwards to obtain
the original input of a computation. The implications are that this
study forms the base of programming languages for reversible CMOS
techology and quantum computing.
technology and quantum computing.

Usually when we add formality to a process, there is a need for
changing the original informal description. Formality enforces us to
Expand Down Expand Up @@ -92,7 +92,7 @@ \section{Why \coq{}}
\coq{} supports proof automation where parts of proofs are done
automatically by the computer. However, most of the time carrying out
proofs are spent on things other than the proof structure: a
considerable amount of time is spent on figuring out how to condiuct
considerable amount of time is spent on figuring out how to conduct
the proof. Another time consumer is feeding the necessary prior
knowledge to the proof system for the development. You can only carry
out 32-bit addition if the system knows, by definition, what a 32-bit
Expand Down Expand Up @@ -173,7 +173,7 @@ \section{Reversible computation}
preservation is carefully chosen such that there \emph{is} an input
yielding the given output. The output space is then the image of all
possible inputs, automatically making the statement surjective on the
codomain.
co-domain.

For a reversible programming language, like JANUS, we obtain the
information preservation by means of an inversion property: Any
Expand All @@ -184,7 +184,7 @@ \section{Reversible computation}
JANUS is reversible because it is possible to define a term-rewriting
system for turning a program into its inverse. We will see that it is
possible since each atomic instruction is invertible and each compound
instruction is invertible if its subcomponents are. This let us use an
instruction is invertible if its components are. This let us use an
inductive argument to show all programs reversible.

%%% Local Variables:
Expand Down
2 changes: 1 addition & 1 deletion report/master.tex
Expand Up @@ -38,10 +38,10 @@
\newcommand{\NN}{\mathbb{N}}
\newcommand{\ZZ}{\mathbb{Z}}

\fixme{Ispell from here once we have it all}
\fixme{Ispell from here once everything is finished}
\fixme{Read through the intro, correcting}
\input{intro}
\fixme{Ispell from here once we have it all}
\fixme{Read through the CocExt, correcting}
\input{cocext}
\fixme{Read through J0, correcting}
Expand Down

0 comments on commit 313b2e4

Please sign in to comment.