From 6b082ddb9512e0fc4348d4700cd785228393568d Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Sun, 21 Jan 2018 21:20:06 0500
Subject: [PATCH] books/bookvol10.1 add SPDE chapter
Goal: Axiom Literate Programming

books/bookvol10.1.pamphlet  250 +++++++++++++++++++++++++++++++++++++++++
changelog  2 +
patch  182 +
src/axiomwebsite/patches.html  2 +
4 files changed, 256 insertions(+), 180 deletions()
diff git a/books/bookvol10.1.pamphlet b/books/bookvol10.1.pamphlet
index d76b876..d4d5d16 100644
 a/books/bookvol10.1.pamphlet
+++ b/books/bookvol10.1.pamphlet
@@ 19534,6 +19534,256 @@ Forcing any important facts by making a class which implements a
particular inferface would then ruin any chance of reattaining
multiple inheritance.
+\chapter[Symmetries of Partial Differential Equations]
+{Symmetries of Partial Differential Equations by Fritz Schwarz}
+
+This chapter is based on Schwarz \cite{Schw87} ``Programming with
+Abstract Data Types: The Symmetry Package SPDE in Scratchpad''.
+
+\section{Symmetries of Differential Equations and the Scratchpad Package SPDE}
+
+Symmetry analysis is the only systematic way to obtain solutions of
+differential equations. Yet it is rarely applied for that purpose and
+most textbooks do not even mention it. The reason is probably the
+enormous amount of calculations which is usually involved in obtaining
+the symmetry group of a given differential equation. Therefore the
+Scratchpad package SPDE which stands for Symmetries of Partial
+Differential Equations has been developed which returns the complete
+symmetry group for a wide class of differential equations
+automatically. As far as the mathematics is
+concerned, only those formulas are given which are a prerequisite for
+the main topic mentioned. The details and many examples may be found
+in the recent review article on that subject by the author [14].
+
+We consider the most general case of a system of differential
+equations for an arbitrary number $m$ of the unknown functions
+$u^\alpha$ which may depend on $n$ arguments $x_i$. These variables
+are collectively denoted by $u=(u^1,\ldots,u^m)$ and
+$x=(x_1,\ldots,x_n)$ respectively. We write the system of $N$
+differential equations in the form
+\[w_\nu(x_i,u^\alpha,u_i^\alpha,u_{ij}^\alpha,\ldots,
+u_{i_1\ldots i_k}^\alpha)=0\eqno{(1)}\]
+for $\nu=1\ldots N$ where the notation
+\[u_{i_1\ldots i_n}^\alpha=\frac{\partial^{i_1+\ldots i_n}u^\alpha}
+{\partial x_1^{i_1}\ldots \partial x_n^{i_n}}\]
+for derivatives has been used. Furthermore it is assumed that the
+equations (1) are polynomial in all arguments. For $m=n=N=1$ a single
+ordinary differential equation is obtained.
+
+To formulate the condition for the invariance of (1), the
+infinitesimal generator $U$ is defined by
+\[U=\xi_i\frac{\partial}{\partial x_i}
++\eta^\alpha\frac{\partial}{\partial u^\alpha}\eqno{(2)}\]
+where $\xi_i$ and $\eta^\alpha$ may depend on all dependent and
+independent variables. Summation over twice occuring indices is always
+assumed. Greek indices run from 1 to $m$ and latin indices from 1 to
+$n$. The $k$th prolongation of $U$ is defined as
+\[U^{(k)}=U+\zeta_i^\alpha\frac{\partial}{\partial u_i^\alpha}+
+\ldots+\zeta_{i_1\ldots i_k}^\alpha
+\frac{\partial}{\partial u_{i_1\ldots i_k}^\alpha}\eqno{(3)}\]
+where the functions $\zeta_{i_1,\ldots i_k}^\alpha$ describe the
+transformation of partial derivatives of order $k$. The $\zeta$'s
+satisfy the recursion relations
+\[\zeta_i^\alpha=D_i(\eta^\alpha)u_s^\alpha D_i(\xi_s)\eqno{(4)}\]
+and
+\[\zeta_{i_1,\ldots i_k}^\alpha=D_{i_k}(\zeta_{i_1\ldots i_{k1}}^\alpha)
+u_{i_1,\ldots i_{k1},s}^\alpha D_{i_k}(\xi_s)\eqno{(5)}\]
+\[D_i=\frac{\partial}{\partial x_i}
++ u_i^\alpha\frac{\partial}{\partial u^\alpha}
++ u_{ki}^\alpha\frac{\partial}{\partial u_k^\alpha}
++ u_{kli}^\alpha\frac{\partial}{\partial
+u_{kl}^\alpha}\ldots\eqno{(6)}\]
+is the operator of total derivation with respect to $x_i$. The system
+of differential equations (1) is invariant under the transformations
+of a oneparameter group with the infinitesimal generator (2) if the
+$\xi$'s and $\eta$'s are determined from the conditions
+\[U^{(k)}\omega_\nu=0\quad{\rm when\ all\ }\omega_\nu=0.\eqno{(7)}\]
+
+Under the constraints for the $\omega_\nu$ which have been mentioned
+above, the left hand side of (7) is a polynomial in all its
+variables. Because the derivatives of the $u$'s do not occur as
+arguments of the $\xi$'s and the $\eta$'s, it has to be decomposed with
+respect to these derivatives and the coefficients are equated to
+zero. The resulting set of equations is the determining system the
+general solution of which determines the full symmetry group of
+(1). Starting from a certainset of simplification rules, a solution
+algorithm has been designed which is described in detail in a separate
+article \cite{Schw85}. The implementation of this algorithm forms the main
+part of the package SPDE wich comprises about 1500 lines of Scratchpad
+code.
+
+Due to its size, the crucial part of the implementation is to identify
+a set of datatypes such that a modularization is obtained. This is not
+a single step process but involves a lot of trial and error and also
+some backtracking. The basic building block for these new datatypes in
+the Scratchpad domain SMP(R,VarSet) which abbreviates Sparse
+Multivariate Polynomial in the VarSet over a ring R. The latter may be
+e.g. the integers, the rational numbers or another polynomial ring
+over some set of variables. There are three basic variables
+distinguished which occur in equations (1) to (7). These are the $x_i$
+and $u^\alpha$, the derivatives $u_{i_1,\ldots i_k}^\alpha$ and the
+differential operaotrs ${\partial}/{\partial x_i}$ and
+${\partial}/{\partial u^\alpha}$. They are represented in
+Scratchpad Symbols of the type DEVAR, DER, and DO
+respectively. Furthermore there are the $\xi$'s and the $\eta$'s
+together with the $c_k$'s which are introduced by the solution
+algorithm. These variables of the type LDFV are also Scratchpad
+Symbols. However they are special in the sense that they carry
+dependencies with them which may change while the solution algorithm
+proceeds. The bookkeeping for these dependencies is organized in terms
+of a Scratchpad association list. For reasons that will become clear
+soon it is advantageous to introduce still another kind of variables
+of type DK which represent the derivatives of the previously introduced
+variables LDFV. They do not correspond straightforwardly to a
+Scratchpad system type.
+
+Out of these variables all quantities which occur may be built up in
+terms of SMP's as follows. The differential equations themselves are
+considered as polynomials in the derivatives of
+$u_{i_1,\ldots i_k}^\alpha$ with coefficients which are polynomials in
+the $x_i$ and $u^\alpha$ over the rationals, i.e. their type is
+SMP(SMP(RN,DEV),DER). The $\zeta$'s are linear polynomials in the
+$\xi$'s, the $\eta$'s and derivatives thereof with coefficients
+which are polynomials in the derivates $u_{i_1,\ldots i_k}^\alpha$
+over the integers, i.e. the appropriate type is
+SMP(SMP(I,DER),DK). The equations of the determining system are
+obtained by decomposing the left hand side of (7) with respect to the
+derivatives $u_{i_1,\ldots i_k}^\alpha$. The resulting equations of
+the determining system are linear polynomials in the DK's with
+coefficients which are polynomials in the variables $x_i$ and
+$u^\alpha$ over the rational numbers. They are denoted by the new type
+LDF. The symmetry generators which are obtained from the solution of
+the determining system are linear polynomials in the differential
+operators $\partial/\partial x_i$ and $\partial/\partial
+u^\alpha$. Depending on whether or not there is a functional
+dependency involved in the final solution their coefficients are LDF's
+or polynomials in the DEV's over the rational numbers respectively. So
+the two kinds of generators are SMP(LDF,DO)'s or SMP(SMP(RN,DEV),DO)'s
+for which the two type CSG and DSG respectively are introduced. The
+complete set of domains of the symmetry package SPDE is listed below
+where the full names are also given.
+
+\begin{tabular}{ccc}
+\hline
+Abbreviation & Full Name & Scratchpad Datatype\\
+\hline
+SPDE & SymmetricPartialDifferentialEquation & Package\\
+\hline
+CSG & ContinuousSymmetryGenerator & SMP(LDF,DO)\\
+\hline
+DSG & DiscreteSymmetryGenerator & SMP(SMP(RN,DEV),DO)\\
+\hline
+DS & DeterminingSystem & List List LDF\\
+\hline
+LDF & LinearDifferentialForm & SMP(SMP(RN,DEV),DK)\\
+\hline
+DK & DifferentialKernel & New Domain\\
+\hline
+LDFV & LDFVariable & Symbol\\
+\hline
+DE & DifferentialEquation & SMP(SMP(RN,DEV),DER)\\
+\hline
+DER & Derivative & Symbol\\
+\hline
+DO & DifferentialOperator & Symbol\\
+\hline
+DEV & DEVariable & Symbol\\
+\hline
+\end{tabular}
+
+An abstract data type is realized in Scratchpad in terms of a domain
+constructor. As an example in the following figure the specification
+of the domain DifferentialKernel is shown. According to the principles
+of Scratchpad, there is a public or category part Cat and a
+private part Tar. The category part Cat defines the outside view. It
+consists of the syntax specification for the exported functions in
+terms of its modemaps and the semantic part in which the meaning of
+these functions is specified. A modemap for a function is a statement
+which determines the number and the types of its arguments and the
+type of the object it returns. Instead of a so called axiomatic or
+algebraic specification a concise and precise description of the
+action of each function in plain English is preferred. It is included
+as a comment in the domain constructor. Analogously the private part
+Tar specifies the syntax and the semantics of the internal
+functions. The difference between the public and the private part
+should be noted. In the former there is no mention whatsoever of the
+internal representation of these objects in terms of certain records.
+The semantic specification is mostly given in mathematical terms. On
+the contrary, in the private part the internal representation of these
+quantities is established. The terms which are used in its
+specification are typical for the Scratchpad system.
+
+The function randDK is a random generator for DK's. Its two arguments
+specify the values of rn and n. It works according to the following
+algorithm. At first a variable of the type LDFV is created by calling
+the random generator from the corresponding domain LDFV. Then a random
+integer between 0 and 5 is generated which specifies an upper bound
+for the total order of the kernel to be returned. Finally in a loop
+the derivatives with respect to the various arguments are determined
+by generating random integers between 0 and 5. The loop terminates if
+the total order is exceeded. In this way DK's are obtained which cover
+fairly uniformly the parameter space which is expected to be relevant
+for applications of the full package, including special cases like
+e.g. 0th order derivatives. This random generator for DK's is called
+by the test program testDK and by test programs for other domains like
+e.g. LDF. The details of this testing process will be discussed later
+in this Section. The domain constructors for the other datatypes are
+similarly organized. The reason for choosing DK as an example has been
+that it is short enough to be reproduced on a single page but still
+contains all the relevant details.
+
+\begin{verbatim}
+)abbreviate domain DK DifferentialKernel
+DifferenetialKernel: Cat == Tar where
+ I ==> Integer
+ DEV ==> DEVariable
+ LDFV ==> LDFVariable
+ VAR ==> Record(Var: DEV, Ord: Integer)
+ Cat == OrderedSet with
+ funDK: $ > LDFV  function argument
+ varDK: $ > List DEV  derivative variables
+ zeroDK: $ > Boolean  true if derivative is 0
+ newKD: LDFV > $  creates DK of 0th order from argument
+ difDK: ($,DEV) > $  derivative w.r.t 2nd argument
+ intDK: ($,DEV) > $  integration w.r.t 2nd argument
+ ordDK: $ > I  total order of derivative
+ ordDK: ($,DEV) > I  order w.r.t 2nd argument
+ oneDK: List $ > LIst $  list elements occuring once
+ randDK: (I,I) > $  generates random DK
+ testDK: (I,I,I,I) > Void  test program
+ coerce: $ > E  print function
+ Tar == add
+ Rep := Record(fn: LDFV, args: List VAR)
+ mkDfL: (List VAR,DEV) > List VAR
+  creates record VAR for derivative
+ mkIntL: (List VAR,DEV) > List Var
+  creates record VAR for integral
+ creDK: (LDFV,List VAR) > $
+  creates DK from LDFV and record VAR
+ VarDK: $ > List VAR
+  returns record VAR of argument
+\end{verbatim}
+
+After the various modules which build up the full package SPDE have
+been established~ their mutual relations have to be investigated. All
+dependencies between the modules are most clearly seen from the
+structure chart which is shown in Figure 4. It makes obvious the
+hierarchical order between the various modules which is based on the
+datatypes. The treelike appearance reflects the most valuable feature
+of the design, i.e. the partial independence among the modules. For
+example, those at the bottom which belong to the level of symbols and
+kernels are almost completely independent from each other. The same is
+true at the next level of the SMP~s. Only at the uppermost level a
+strong interconneetion is established among the modules of the full
+package due to the operations of the module SPDE. This is not
+surprising however since it is the task of that latter module to
+organize the cooperation within the package. This becomes clear
+already from the fact that SPDE is a Scratchpad package constructor
+whereas all other modules are domain constructors. To emphasize this
+significant difference~ the interconnections between modules have been
+marked with heavy ~nes whereas for all dependencies on the package
+constructor SPDE thin lines are applied.
+
\chapter{Finite Fields in Axiom (Grabmeier/Scheerhorn)}
This was written by Johannes Grabmeier and Alfred Scheerhorn.
diff git a/changelog b/changelog
index fcbf79a..55cae47 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20180121 tpd src/axiomwebsite/patches.html 20180121.02.tpd.patch
+20180121 tpd books/bookvol10.1 add SPDE chapter
20180121 tpd src/axiomwebsite/patches.html 20180121.01.tpd.patch
20180121 tpd books/bookvolbib add references
20180119 tpd src/axiomwebsite/patches.html 20180119.03.tpd.patch
diff git a/patch b/patch
index c8781e5..f311942 100644
 a/patch
+++ b/patch
@@ 1,181 +1,3 @@
books/bookvolbib add references
+books/bookvol10.1 add SPDE chapter
Goal: Proving Axiom Correct

\index{Harper, Robert}
\begin{chunk}{axiom.bib}
@book{Harp11,
 author = "Harper, Robert",
 title = {{Programming in Standard ML}},
 year = "2011",
 publisher = "CMU",
 keywords = "printed"
}

\end{chunk}

\index{Zippel, Richard}
\begin{chunk}{axiom.bib}
@book{Zipp92,
 author = "Zippel, Richard",
 title = {{Algebraic Computation}},
 publisher = "Cornell University",
 comment = "Unpublished",
 year = "1992",
 keywords = "axiomref, printed"
}

\end{chunk}

\index{Schwarz, Fritz}
\begin{chunk}{axiom.bib}
@article{Schw88,
 author = "Schwarz, Fritz",
 title = {{Symmetries of Differential Equations: From Sophus Lie to
 Computer Algebra}},
 journal = "SIAM Review",
 volume = "30",
 number = "3",
 year = "1988",
 abstract =
 "The topic of this article is the symmetry analysis of
 differential equations and the applications of computer algebra to
 th extensive analytical calculations which are usually involved in
 it. The whole area naturally decomposes into two parts depending
 on whether ordinary or partial differential equations are
 considered. We show how a symmetry may be applied to lower the
 order of an ordinary differential equation or to obtain similarity
 solutions of partial differential equations. The computer algebra
 packages SODE and SPDE, respectively, which have been developed to
 perform almost all algebraic manipulations necessary to determine
 the symmetry group of a given differential equation, are
 presented. Futhermore it is argued that the application of
 computer algebra systems has qualitatively changed this area of
 applied mathematics",
 keywords = "axiomref, printed"
}

\end{chunk}

\index{Garcia, Ronald}
\index{Clark, Alison M.}
\index{Tanter, Eric}
\begin{chunk}{axiom.bib}
@inproceedings{Garc16,
 author = "Garcia, Ronald and Clark, Alison M. and Tanter, Eric",
 title = {{Abstracting Gradual Typing}},
 booktitle = "POPL 16",
 publisher = "ACM",
 year = "2016",
 pages = "429442",
 abstract =
 "Language researchers and designers have extended a wide variety
 of type systems to support {\sl gradual typing}, which enables
 languages to seemlessly combine dynamic and static checking. These
 efforts consistently demonstrate that designing a satisfactory
 gradual counterpart to a static type system is challenging, and
 this challenge only increases with the sophistication of the type
 system. Graudal type system designers need more formal tools to
 help them conceptualize, structure, and evaluate their designs.

 In this paper, we propose a new formal foundation for graudal
 typing, drawing on principles from abstract interpretation to give
 gradual types a semantics in terms of preexisting static
 types. Abstracting Gradual Typing (AGT for short) yields a formal
 account of {\sl consistency}  one of the cornerstones of the
 gradual typing approach  that subsumes existing notions of
 consistency, which were developed through intuition and ad hoc
 reasoning.

 Given a syntaxdirected static typing judgment, the AGT approach
 induces a corresponding gradual typing judgment. Then the type
 safety proof for the underlying static discipline induces a
 dynamic semantics for gradual programs defined over
 sourcelanguage typing derivations. The AGT approach does not
 resort to an externally justified cast calculus; instead, runtime
 check naturally arise by deducing evidence for consistent
 judgements during proof reduction.

 To illustrate the approach, we develop a novel graduallytyped
 counterpart for a language with record subtyping. Gradual
 languages designed with the AGT approach satisfy {\sl by
 construction} the refined criteria for gradual typing set forth by
 Siek and colleagues.",
 keywords = "printed"
}

\end{chunk}

\index{Garcia, Ronald}
\index{Cimini, Matteo}
\begin{chunk}{axiom.bib}
@inproceedings{Garc17,
 author = "Garcia, Ronald and Cimini, Matteo",
 title = {{Principal Type Schemes for Gradual Programs}},
 booktitle = "POPL 15",
 comment = "Updated paper",
 year = "2017",
 abstract =
 "Gradual typing is a discipline for integrating dynamic checking
 into a static type system. Since its introduction in functional
 languages, it has been adapted to a variety of type systems,
 including objectoriented, security, and substructural. This work
 studies its application to implictly typed languages based on type
 inference. Siek and Vachharajani designed a gradual type inference
 system and algorithm that infers gradual types but still rejects
 illtyped static programs. However, the type system requires local
 reasoning about type substitutions, an imperative inference
 algorithm, and a subtle correctness statement.

 This paper introduces a new approach to gradual type inference,
 driven by the principle that gradual inference should only produce
 static types. We present a static implicitly typed language, its
 gradual counterpart, and a type inference procedure. The gradual
 system types the same programs as Siek and Vachharajani, but has a
 modular structure amenable to extension. The language admits
 letpolymorphism, and its dynamics are defined by translation to
 the Polymorphic Blame Calculus (Ahmed et al. 2009, 2011).

 The principal types produced by our initial type system mask the
 distinction between static parametric polymorphism and
 polymorphism that can be attributed to gradual typing. To expose
 this difference, we distinguish static type parameters from
 gradual type parameters and reinterpret gradual type consistency
 accordingly. The resulting extension enables programs to be
 interpreted using either the polymorphic or monomorphic Blame
 Calculi.",
 keywords = "printed"
}

\end{chunk}

\index{Brady, Edwin}
\begin{chunk}{axiom.bib}
@article{Brad13,
 author = "Brady, Edwin",
 title = {{Idris, a General Purpose Dependently Typed Programming
 Language: Design and Implementation}},
 journal = "J. Functional Programming",
 volume = "23",
 number = "5",
 year = "2013",
 pages = "552593",
 abstract =
 "Many components of a dependently typed programming language are by
 now well understood, for example, the underlying type theory, type
 checking, unification and evaluation. How to combine these components
 into a realistic and usable highlevel language is, however, folklore,
 discovered anew by successive language implementors. In this paper, I
 describe the implementation of Idris, a new dependently typed
 functional programming language. Idris is intended to be a
 generalpurpose programming language and as such provides highlevel
 concepts such as implicit syntax, type classes and do notation. I
 describe the highlevel language and the underlying type theory, and
 present a tacticbased method for elaborating concrete highlevel
 syntax with implicit arguments and type classes into a fully explicit
 type theory. Furthermore, I show how this method facilitates the
 implementation of new highlevel language constructs.",
 keywords = "printed"
}

\end{chunk}
+Goal: Axiom Literate Programming
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index fc0f73b..cade940 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5902,6 +5902,8 @@ books/bookvolbib add references
books/bookvol13 add Berg95
20180121.01.tpd.patch
books/bookvolbib add references
+20180121.02.tpd.patch
+books/bookvol10.1 add SPDE chapter

1.9.1