From 107845ec7eea79108b611cb8bbcd1e05588ed6fd Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Fri, 10 Mar 2017 00:33:50 -0500
Subject: [PATCH] books/bookvolbib Homotopy Type Theory reference
Goal: Proving Axiom Correct
\index{Harper, Robert}
\begin{chunk}{axiom.bib}
@misc{Harp13,
author = "Harper, Robert",
title = "15.819 Homotopy Type Theory Course",
link = "\url{http://www.cs.cmu.edu/~rwh/courses/hott}",
year = "2013"
}
\end{chunk}
---
books/bookvol13.pamphlet | 8 ++
books/bookvolbib.pamphlet | 191 ++++++++++++++++++++++++++++++++++++++--
changelog | 2 +
patch | 16 +++-
src/axiom-website/patches.html | 2 +
5 files changed, 209 insertions(+), 10 deletions(-)
diff --git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index 1e76f47..d72ca40 100644
--- a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ -103,6 +103,14 @@ always boring if the definitions are right.
A: The definitions are almost always wrong.
\end{quote}
+\begin{quote}
+Type theory is nothin short of a grand unified theory of computation
+unified with mathematics so ultimately there is no difference between
+math and the code.
+
+-- Robert Harper\cite{Harp13}
+\end{quote}
+
\chapter{Here is a problem}
Proving programs correct involves working with a second programming
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 5c3e2d8..8d2afb5 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -5555,6 +5555,47 @@ Martin, U.
\end{chunk}
+\index{Baumgartner, Gerald}
+\index{Stansifer, Ryan}
+\begin{chunk}{axiom.bib}
+@techreport{Baum90,
+ author = "Baumgartner, Gerald and Stansifer, Ryan",
+ title = "A Proposal to Study Type Systems for Computer Algebra",
+ institution = "RISC",
+ year = "1990",
+ type = "technical report",
+ number = "90-07.0",
+ abstract =
+ "It is widely recognized that programming languages should offer
+ features to help structure programs. To achieve this goal, languages
+ like ADA, MODULA-2, object-oriented languages, and functional
+ languages have been developed. The structuring techniques available so
+ far (like modules, classes, parametric polymorphism) are still not
+ enough or not appropriate for some application areas. In symbolic
+ computation, in particular computer algebra, several problems occur
+ that are difficult to handle with any existing programming language.
+ Indeed, nearly all available computer algebra systems suffer from the
+ fact that the underlying programming language imposes too many
+ restricitons.
+
+ We propose to develop a language that combines the essential features
+ from functional language, object-oriented languages, and computer
+ algebra systems in a semantically clean manner. Although intended for
+ use in symbolic computation, this language should prove interesting as
+ a general purpose programming language. The main innovation will be
+ the application of sophisticated type systems to the needs of computer
+ algebra systems. We will demonstrate the capabilities of the language
+ by using it to implement a small computer algebra library. This
+ implementation will be compared against a straightforward Lisp
+ implementation and against existing computer algebra systems. Our
+ development should have an impact both on the programming languages
+ world and on the computer algebra world.",
+ paper = "Baum90.pdf",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
\index{Beeson, Michael}
\begin{chunk}{axiom.bib}
@misc{Beesxx,
@@ -6013,6 +6054,35 @@ Martin, U.
\end{chunk}
+\index{Comon, H.}
+\index{Lugiez, D.}
+\index{Schnoebelen, P.H.}
+\begin{chunk}{axiom.bib}
+@article{Como88,
+ author = "Comon, H. and Lugiez, D. and Schnoebelen, P.H.",
+ title = "A Rewrite-based Type Discipline for a Subset of Computer Algebra",
+ journal = "J. Symbolic Computation",
+ year = "1991",
+ volume = "11",
+ pages = "349-368",
+ abstract =
+ "This paper is concerned with the type structure of a system including
+ polymorphism, type properties, and subtypes. This type system
+ originates from computer algebra but it is not intended to be the
+ solution of all type problems in this area.
+
+ Types (or sets of types) are denoted by terms in some order-sorted
+ algebra. We consider a rewrite relation in this algebra, which is
+ intended to express subtyping. The relations between the semantics and
+ the axiomatization are investigated. It is shown that the problem of
+ type inference is undecidable but that a narrowing strategy for
+ semi-decision procedures is described and studied.",
+ paper = "Como88.pdf",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
\index{Coquand, Thierry}
\index{Huet, G\'erard}
\begin{chunk}{axiom.bib}
@@ -6758,6 +6828,17 @@ Calculemus (2011) Springer
\end{chunk}
+\index{Harper, Robert}
+\begin{chunk}{axiom.bib}
+@misc{Harp13,
+ author = "Harper, Robert",
+ title = "15.819 Homotopy Type Theory Course",
+ link = "\url{http://www.cs.cmu.edu/~rwh/courses/hott}",
+ year = "2013"
+}
+
+\end{chunk}
+
\index{Heeren, Bastiaan}
\index{Hage, Jurriaan},
\index{Swierstra, Doaitse}
@@ -7936,6 +8017,21 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\subsection{R} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Rector, D. L.}
+\begin{chunk}{axiom.bib}
+#InCollection{Rect89,
+ author = "Rector, D. L.",
+ title = "Semantics in Algebraic Computation",
+ booktitle = "Computers and Mathematics",
+ publisher = "Springer-Verlag",
+ year = "1989",
+ pages = "299-307",
+ isbn = "0-387-97019-3",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
\index{Roberts, Siobhan}
\begin{chunk}{axiom.bib}
@misc{Robe15,
@@ -9037,7 +9133,8 @@ J. Symbolic Computation (1998) Vol 26 pp607-619
\index{Weber, Andreas}
\begin{chunk}{ignore}
\bibitem[Weber 06]{Webe06} Weber, Andreas
- title = "Quantifier Elimination on Real Closed Fields and Differential Equations",
+ title = "Quantifier Elimination on Real Closed Fields and Differential
+ Equations",
link = "\url{http://cg.cs.uni-bonn.de/personal-pages/weber/publications/pdf/WeberA/Weber2006a.pdf}",
keywords = "survey",
abstract = "
@@ -25133,6 +25230,7 @@ in [Wit87], pp5-8
have a form that is closely related to the algorithmic description of
a problem, but with the security of full type checking in a compact,
natural style.",
+ paper = "Hear95.pdf",
keywords = "axiomref"
}
@@ -33945,13 +34043,90 @@ IBM T. J. Watson Research Center (2001)
school = "University of Tubingen",
year = "1993",
abstract =
- "An important feature of modern computer algebra systems is the support
- of a rich type system with the possibility of type inference. Basic
- features of such a type system are polymorphism and coercion between
- types. Recently the use of order-sorted rewrite systems was proposed
- as a general framework. We will give a quite simple example of a
- family of types arising in computer algebra whose coercion relations
- cannot be captured by a finite set of first-order rewrite rules.",
+ "We study type systems for computer algebra systems, which frequently
+ correspond to the ``pragmatically developed'' typing constructs used
+ in AXIOM.
+
+ A central concept is that of type classes which correspond to AXIOM
+ categories. We will show that types can be syntactically described as
+ terms of a regular order-sorted signature if no type parameters are
+ allowed. Using results obtained for the functional programming
+ language Haskell we will show that the problem of type inference is
+ decidable. This result still holds if higher-order functions are
+ present and parametric polymorphism is used. These additional typing
+ constructs are useful for further extensions of existing computer
+ algebra systems: These typing concepts can be used to implement
+ category theoretic constructs and there are many well known
+ constructive interactions between category theory and algebra.
+
+ On the one hand we will show that there are well known techniques to
+ specify many important type classes algebraically, and we will also
+ show that a formal and algorithmically Feasible treatment of the
+ interactions of algebraically specified data types and type classes is
+ possible. On the other hand we will prove that there are quite
+ elementary examples arising in computer algebra which need very
+ ``strong'' formalisms to be specified and are thus hard to handle
+ algorithmically.
+
+ We will show that it is necessary to distinguish between types and
+ elements as parameters of parameterized type classes. The type
+ inference problem for the former remains decidable whereas for the
+ latter it becomes undecidable. We will also show that such a
+ distinction can be made quite naturally.
+
+ Type classes are second-order types. Although we will show that there
+ are constructions used in mathematics which imply that type classes
+ have to become first-order types in order to model the examples
+ naturally, we will also argue that this does not seem to be the case
+ in areas currently accessible for an algebra system. We will only
+ sketch some systems that have been developed during the last years in
+ which the concept of type classes as first-order types can be
+ expressed. For some of these systems the type inference problem was
+ proven to be undecidable.
+
+ Another fundamental concept for a type system of a computer algebra
+ system — at least for the purpose of a user interface — are coercions.
+ We will show that there are cases which can be modeled by coercions
+ but not by an ``inheritance mechanism'', i. e. the concept of coercions
+ is not only orthogonal to the one of type classes but also to more
+ general formalisms as are used in object-oriented languages. We will
+ define certain classes of coercions and impose conditions on important
+ classes of coercions which will imply that the meaning of an expression
+ is independent of the particular coercions that are used in order to
+ type it.
+
+ We shall also impose some conditions on the interaction between
+ polymorphic operations defined in type classes and coercions that will
+ yield a unique meaning of an expression independent of the type which
+ is assigned to it — if coercions are present there will very
+ frequently be several possibilities to assign types to expressions.
+
+ Often it is not only possible to coerce one type into another but it
+ will be the case that two types are actually isomorphic . We will
+ show that isomorphic types have properties that cannot be deduced from
+ the properties of coercions and will shortly discuss other possibilities
+ to model type isomorphisms. There are natural examples of type
+ isomorphisms occurring in the area of computer algebra that have
+ a ``problematic'' behavior. So we will prove for a certain example that
+ the type isomorphisms cannot be captured by a finite set of coercions
+ by proving that the naturally associated equational theory is not
+ finitely axiomatizable.
+
+ Up to now few results are known that would give a clear dividing line
+ between classes of coercions which have a decidable type inference
+ problem and classes for which type inference becomes undecidable.
+ We will give a type inference algorithm for some important classes of
+ coercions.
+
+ Other typing constructs which are again quite orthogonal to the
+ previous ones are those of {\sl partial functions} and of types
+ {\sl depending on elements} . We will link the treatment of {\sl partial
+ functions} in AXIOM to the one used in order-sorted algebras and will
+ show some problems which arise if a seemingly more expressive solution
+ were used. There are important cases in which {\sl types depending on
+ elements} arise naturally. We will show that not only type inference
+ but even type checking is undecidable for relevant cases occurring in
+ computer algebra.",
paper = "Webe93b.pdf",
keywords = "axiomref"
}
diff --git a/changelog b/changelog
index fbd7389..7ffd2a1 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20170310 bmt src/axiom-website/patches.html 20170310.01.tpd.patch
+20170310 tpd books/bookvolbib Homotopy Type Theory reference
20170309 bmt src/axiom-website/patches.html 20170309.01.bmt.patch
20170309 bmt books/Makefile add tanglec to $AXIOM/bin
20170308 bmt src/axiom-website/patches.html 20170308.01.bmt.patch
diff --git a/patch b/patch
index 999014d..a3296bd 100644
--- a/patch
+++ b/patch
@@ -1,4 +1,16 @@
-books/Makefile add tanglec to $AXIOM/bin
+books/bookvolbib Homotopy Type Theory reference
+
+Goal: Proving Axiom Correct
+
+\index{Harper, Robert}
+\begin{chunk}{axiom.bib}
+@misc{Harp13,
+ author = "Harper, Robert",
+ title = "15.819 Homotopy Type Theory Course",
+ link = "\url{http://www.cs.cmu.edu/~rwh/courses/hott}",
+ year = "2013"
+}
+
+\end{chunk}
-Goal: Feature request
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 1ab9614..2107c25 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5674,6 +5674,8 @@ books/bookvolbug fix bug 7324: MATLIN fractionFreeGauss! elt error

books/bookvol10 add src/algebra/*.spad to binary distro

20170309.01.bmt.patch
books/Makefile add tanglec to $AXIOM/bin

+20170310.01.tpd.patch
+books/bookvolbib Homotopy Type Theory reference

--
1.7.5.4