-
Notifications
You must be signed in to change notification settings - Fork 54
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
src/input/quantunwalk.input Code for quantum walk from McGettrick
Goal: Axiom Test Code
- Loading branch information
Showing
5 changed files
with
128 additions
and
298 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,296 +1,4 @@ | ||
| books/bookvolbib Axiom Citations in the Literature | ||
| src/input/quantunwalk.input Code for quantum walk from McGettrick | ||
|
|
||
| Goal: Axiom Literate Programming | ||
|
|
||
| Collect algebra references in the bibliography | ||
|
|
||
| \index{Carette, Jacques} | ||
| \index{Kiselyov, Oleg} | ||
| \begin{chunk}{axiom.bib} | ||
| @article{Care11, | ||
| article = "Carette, Jacques and Kiselyov, Oleg", | ||
| title = "Multi-stage programming with functors and monads: eliminating | ||
| abstraction overhead from generic code", | ||
| journal = "Sci. Comput. Program", | ||
| volume = "76", | ||
| number = "5", | ||
| pages = "349-375", | ||
| year = "2011", | ||
| paper = "Care11.pdf", | ||
| url = "http://www.cas.mcmaster.ca/~carette/metamonads/metamonads.pdf", | ||
| keywords = "axiomref", | ||
| abstract = | ||
| "We use multi-stage programming, monads and OCaml's advanced module | ||
| system to demonstrate how to eliminate all abstraction overhead from | ||
| generic programs, while avoiding any inspection of the resulting code. | ||
| We demonstrate this clearly with Gaussian Elimination as a | ||
| representative family of symbolic and numeric algorithms. We | ||
| parameterize our code to a great extent -- over domain, input and | ||
| permutation matrix representations, determinant and rank tracking, | ||
| pivoting policies, result types, etc. -- at no run-time cost. Because | ||
| the resulting code is generated just right and not changed afterward, | ||
| MetoOCaml guarantees that the generated code is well-typed. We further | ||
| demonstrate that various abstraction parameters (aspects) can be made | ||
| orthogonal and compositional, even in the presence of name-generation | ||
| for temporaries, and ``interleaving'' of aspects. We also show how to | ||
| encode some domain-specific knowledge so that ``clearly wrong'' | ||
| compositions can be rejected at or before generation time, rather than | ||
| during the compilation or running of the generated code." | ||
| } | ||
|
|
||
| \end{chunk} | ||
|
|
||
| \index{Rojas-Bruna, Carlos} | ||
| \begin{chunk}{axiom.bib} | ||
| \article{Roja13, | ||
| author = "Rojas-Bruna, Carlos", | ||
| title = "Trace forms and ideals on commutative algebras satisfying an | ||
| identity of degree four", | ||
| journal = "Rocky Mt. J. Math.", | ||
| year = "2013", | ||
| volume = "43", | ||
| number = "4", | ||
| pages = "1325-1336", | ||
| keywords = "axiomref", | ||
| abstract = | ||
| "This paper deals with the variety of commutative algebras satsifying | ||
| the identity | ||
| \[((xy)z)t - ((xy)t)z + ((yt)x)z - ((yt)z)x + ((yz)t)x - ((yz)x)t = 0\] | ||
| These algebras appeared in the classification of the degree four | ||
| identities in Carini et al. We prove the existence of a trace | ||
| form. Moreover, if we assume the existence of degenerate trace form, | ||
| the $A$ satisfies the identity $((yx)x)x=y((xx)x)$, a generalization | ||
| of right-alternativity. Finally we prove that $Ass[A]$ and $N(A)$ are | ||
| ideals in these algebras." | ||
| } | ||
|
|
||
| \end{chunk} | ||
|
|
||
| \index{Dos Reis, Gabriel} | ||
| \begin{chunk}{axiom.bib} | ||
| \article{Reis12, | ||
| author = "Dos Reis, Gabriel", | ||
| title = "A System for Axiomatic Programming", | ||
| journal = "Proc. Conf. on Intelligent Computer Mathematics", | ||
| publisher = "Springer", | ||
| year = "2012", | ||
| url = "http://www.axiomatics.org/~gdr/liz/cicm-2012.pdf", | ||
| paper = "Reis12.pdf", | ||
| keywords = "axiomref", | ||
| abstract = " | ||
| We present the design and implementation of a system for axiomatic | ||
| programming, and its application to mathematical software | ||
| construction. Key novelties include a direct support for user-defined | ||
| axioms establishing local equality between types, and overload | ||
| resolution based on equational theories and user-defined local | ||
| axioms. We illustrate uses of axioms, and their organization into | ||
| concepts, in structured generic programming as practiced in | ||
| computational mathematical systems." | ||
| } | ||
|
|
||
| \end{chunk} | ||
|
|
||
| \index{Dos Reis, Gabriel} | ||
| \index{Matthews, David} | ||
| \index{Li, Yue} | ||
| \begin{chunk}{axiom.bib} | ||
| @article{Reis11, | ||
| author = "Dos Reis, Gabriel", | ||
| title = "Retargeting OpenAxiom to Poly/ML: towards an integrated proof | ||
| assistants and computer algebra system framework", | ||
| journal = "Intelligent computer mathematics (MKM 2011)", | ||
| year = "2011", | ||
| isbn = "978-3-642-22672-4", | ||
| paper = "Reis11.pdf", | ||
| url = | ||
| "https://www.semanticscholar.org/paper/Retargeting-OpenAxiom-to-PolyML-Towards-an-Reis-Matthews/4ce5d85ea8424ced82d", | ||
| keywords = "axiomref", | ||
| abstract = | ||
| "This paper presents an ongoing effort to integrate the AXIOM family | ||
| of computer algebra systems with Poly/ML-based proof assistants in the | ||
| same framework. A long-term goal is to make a large set of efficient | ||
| implementations of algebraic algorithms available to popular proof | ||
| assistants, and also to bring the power of mechanized formal | ||
| verification to a family of strongly typed computer algebra systems at | ||
| a modest cost. Our approach is based on retargeting the code generator | ||
| of the OpenAxiom compiler to the Poly/ML abstract machine." | ||
| } | ||
|
|
||
| \end{chunk} | ||
|
|
||
| \index{Kredel, Heinz} | ||
| \begin{chunk}{axiom.bib} | ||
| @book{Kred11, | ||
| author = "Kredel, Heinz", | ||
| title = "Unique factorization domains in the Java computer algebra system", | ||
| year = "2011", | ||
| booktitle = "Automated deduction in geometry (ADG 2008)", | ||
| pages = "86-115", | ||
| isbn = "978-3-642-21045-7", | ||
| keywords = "axiomref", | ||
| abstract = | ||
| "This paper describes the implementation of recursive algorithms in | ||
| unique factorization domains, namely multivariate polynomial greatest | ||
| common divisors (gcd) and factorization into irreducible parts in the | ||
| Java computer algebra library (JAS). The implementation of gcds, | ||
| resultants and factorization is part of the essential building blocks | ||
| for any computation in algebraic geometry, in particular in automated | ||
| deduction in geometry. There are various implementations of these | ||
| algorithms in procedural programming languages. Our aim is an | ||
| implementation in a modern object oriented language with generic data | ||
| types, as it is provided by Java programming language. We exemplify | ||
| that the type design and implementation of JAS is suitable for the | ||
| implementation of several greatest common divisor algorithms and | ||
| factorization of multivariate polynomials. Due to the design we can | ||
| employ this package in very general settings not commonly seen in other | ||
| computer algebra systems. As for example, in the coefficient | ||
| arithmetic for advanced Groebner basis computations like in polynomial | ||
| rings over rational function fields or (finite, commutative) regular | ||
| rings. The new package provides factory methods for the selection of | ||
| one of the several implementations for non experts. Further we | ||
| introduce a parallel proxy for gcd implementations which runs | ||
| different implementations concurrently." | ||
| } | ||
|
|
||
| \end{chunk} | ||
|
|
||
| \index{Kredel, Heinz} | ||
| \index{Jolly, Raphael} | ||
| \begin{chunk}{axiom.bib} | ||
| @InProceedings{{Kred11a, | ||
| author = "Kredel, Heinz and Jolly, Raphael", | ||
| title = "Algebraic structures as typed objects", | ||
| booktitle = "Proc. 13th International Workshop", | ||
| series = "CASC 2011", | ||
| year = "2011", | ||
| isbn = "978-3-642-23567-2", | ||
| location = "Berlin", | ||
| pages = "294-308", | ||
| keywords = "axiomref", | ||
| paper = "Kred11a.pdf", | ||
| url = "http://krum.rz.uni-mannheim.de/kredel/to-cas-casc2011-slides.pdf", | ||
| abstract = | ||
| "Following the research direction of strongly typed, generic, object | ||
| oriented computer algebra software, we examine the modeling of | ||
| algebraic structures as typed objects in this paper. We discuss the | ||
| design and implementation of algebraic and transcendental extension | ||
| fields together with the modeling of real algebraic and complex | ||
| algebraic extension fields. We will show that the modeling of the | ||
| relation between algebraic and real algebraic extension fields using | ||
| the delegation design concept has advantages over the modeling as | ||
| sub-types using sub-class implementation. We further present a summary | ||
| of design problems, which we have encountered so far with our | ||
| implementation in Java and present possbile solutions in Scala." | ||
| } | ||
|
|
||
| \end{chunk} | ||
|
|
||
| \index{Spitters, Bas} | ||
| \index{van der Weegen, Eelis} | ||
| \begin{chunk}{axiom.bib} | ||
| @article{Spit11, | ||
| author = "Spitters, Bas and van der Weegen, Eelis", | ||
| title = "Type classes for mathematics in type theory", | ||
| journal = "Math. Struct. Comput. Sci.", | ||
| volume = "21", | ||
| number = "4", | ||
| pages = "795-825", | ||
| year = "2011", | ||
| keywords = "axiomref", | ||
| url = "https://arxiv.org/pdf/1102.1323.pdf", | ||
| paper = "Spit11.pdf", | ||
| abstract = | ||
| "The introduction of first-class type classes in the Coq system calls | ||
| for a re-examination of the basic interfaces used for mathematical | ||
| formalisation in type theory. We present a new set of type classes for | ||
| mathematics and take full advantage of their unique features to make | ||
| practical a particularly flexible approach that was formerly thought | ||
| to be infeasible. Thus, we address traditional proof engineering | ||
| challenges as well as new ones resulting from our ambition to build | ||
| upon this development a library of constructive analysis in which any | ||
| abstraction penalties inhibiting efficient computation are reduced to | ||
| a minimum. | ||
|
|
||
| The basis of our development consists of type classes representing a | ||
| standard algebraic hierarchy, as well as portions of category theory | ||
| and universal algebra. On this foundation, we build a set of | ||
| mathematically sound abstract interfaces for different kinds of | ||
| numbers, succinctly expressed using categorical language and universal | ||
| algebra constructions. | ||
|
|
||
| Strategic use of type classes lets us support these high-level | ||
| theory-friendly definitions, while still enabling efficient | ||
| implementations unhindered by gratuitous indirection, conversion or | ||
| projection. | ||
|
|
||
| Algebra thrives on the interplay between syntax and semantics. The | ||
| Prolog-like abilities of type class instance resolution allow us to | ||
| conveniently define a quote function, thus facilitating the use of | ||
| reflective techniques." | ||
| } | ||
|
|
||
| \end{chunk} | ||
|
|
||
| \index{Kredel, Heinz} | ||
| \index{Jolly, Raphael} | ||
| \begin{chunk}{axiom.bib} | ||
| @InProceedings{{Kred10, | ||
| author = "Kredel, Heinz and Jolly, Raphael", | ||
| title = "Generic, type-safe and object oriented computer algebra software", | ||
| booktitle = "Proc. 12th International Workshop", | ||
| series = "CASC 2010", | ||
| year = "2010", | ||
| isbn = "978-3-642-15273-3", | ||
| location = "Berlin", | ||
| pages = "162-177", | ||
| keywords = "axiomref", | ||
| paper = "Kred10.pdf", | ||
| url = "http://krum.rz.uni-mannheim.de/kredel/oocas-casc2010-slides.pdf", | ||
| abstract = | ||
| "Advances in computer science, in particular object oriented | ||
| programming, and software engineering have had little practical impact | ||
| on computer algebra systems in the last 30 years. The software design | ||
| of existing systems is still dominated by ad-hoc memory management, | ||
| weakly typed algorithm libraries and proprietary domain specific | ||
| interactive expression interpreters. We discuss a modular approach to | ||
| computer algebra software: usage of state-of-the-art memory management | ||
| and run-time systems (e.g. JVM) usage of strongly typed, generic, | ||
| object oriented programming languages (e.g. Java) and usage of general | ||
| purpose, dynamic interactive expression interpreters (e.g. Python). To | ||
| illuatrate the workability of this approach, we have implemented and | ||
| studied computer algebra systems in Java and Scala. In this paper we | ||
| report on the current state of this work by presenting new examples." | ||
| } | ||
|
|
||
| \end{chunk} | ||
|
|
||
| \index{Lecerf, Gr{\'e}goire} | ||
| \begin{chunk}{axiom.bib} | ||
| @InProceedings{{Lece10, | ||
| author = "Lecerf, Gregoire", | ||
| title = "Mathemagix: toward large scale programming for symbolic and | ||
| certified numeric computations", | ||
| booktitle = "Mathematical software", | ||
| series = "ICMS 2010", | ||
| year = "2010", | ||
| isbn = "978-3-642-15581-9", | ||
| location = "Berlin", | ||
| pages = "329-332", | ||
| keywords = "axiomref", | ||
| abstract = | ||
| "Coordinated by Joris van der Hoeven from the 90's, the Mathemagix | ||
| project aims at the design of a scientific programming language for | ||
| symbolic and certified numeric algorithms. This language can be | ||
| compiled and interpreted, and it features a strong type system with | ||
| classes and categories. Several C++ libraries are also being | ||
| developed, mainly with Bernard Mourrain and Philippe Trebuchet, for | ||
| the elementary operations with polynomials, power series and matrices, | ||
| with a special care towards efficiency and numeric stability. | ||
|
|
||
| In my talk I will give an overview of the language, of the design and | ||
| the contents of the C++ libraries, and I will illustrate possibilities | ||
| offered for certified numeric computations with balls and intervals." | ||
| } | ||
|
|
||
| \end{chunk} | ||
| Goal: Axiom Test Code | ||
|
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.