diff --git a/cd/Official/list4.ocd b/cd/Official/list4.ocd new file mode 100644 index 0000000..ebd3fc9 --- /dev/null +++ b/cd/Official/list4.ocd @@ -0,0 +1,511 @@ + +list4 +This CD provides symbols that make it possible to state general FMPs about variadic application symbols, by treating a list of things as the list of children of an OMA element. +http://www.openmath.org/cd +0 2 + + This document is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. + + The copyright holder grants you permission to redistribute this + document freely as a verbatim copy. Furthermore, the copyright + holder permits you to develop any derived work from this document + provided that the following conditions are met. + a) The derived work acknowledges the fact that it is derived from + this document, and maintains a prominent reference in the + work to the original source. + b) The fact that the derived work is not the original OpenMath + document is stated prominently in the derived work. Moreover if + both this document and the derived work are Content Dictionaries + then the derived work must include a different CDName element, + chosen so that it cannot be confused with any works adopted by + the OpenMath Society. In particular, if there is a Content + Dictionary Group whose name is, for example, `math' containing + Content Dictionaries named `math1', `math2' etc., then you should + not name a derived Content Dictionary `mathN' where N is an integer. + However you are free to name it `private_mathN' or some such. This + is because the names `mathN' may be used by the OpenMath Society + for future extensions. + c) The derived work is distributed under terms that allow the + compilation of derived works, but keep paragraphs a) and b) + intact. The simplest way to do this is to distribute the derived + work under the OpenMath license, but this is not a requirement. + If you have questions about this license please contact the OpenMath + society at http://www.openmath.org. + +experimental +2014-07-07 + + islist + application + This symbol is a predicate stating that something (the only argument) is a list. This is useful for making claims of the form “for every list L, it holds that …” in FMPs. + + The list whose elements are the integers 3, 6, and 5 is a list: + + + + 3 + 6 + 5 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + islistwhere + application + This symbol is a predicate of two arguments L and P, where P is a predicate of one argument. The claim expressed is first that L is a list, and second that every element of it satisfies P. + + + + + + + + + + + + + + + + + + + + + + + + + + + + 1 + + + + + + + + + + + + + + + + + + + + + + + + + + eval + application + This is an application symbol which takes an arbitrary number of lists as arguments. The concatenation of those lists should be nonempty. To eval those lists produces the same result as an application (OMA element, in the XML encoding) having the concatenation of them as its list of children. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + In general, if f is any application symbol, and x1, x2, ..., xN is any sequence of arguments, then f(x1,x2,...,xN) is equal to eval(list1.list(f,x1,x2,...,xN)). This infinite sequence of identities cannot be expressed as an FMP, even if every particular element in that sequence can be so expressed, but by accepting it to hold for the eval symbol in particular, it becomes possible to state similar infinite sequences of claims about other symbols as finite FMPs. + + + The second thing one needs to know about eval is that an eval of two lists is the same as an eval of their concatenation. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Finally, to define eval for more than two arguments, we can use nested evaluation with a list-of-lists argument. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + It is a theorem following from the above that an eval of three lists is equal to a two-argument eval of the concatenation of the first two lists and the last list. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + nassoc + application + This symbol is a predicate which takes one operation as argument. It expresses the claim that this operation is n-associative, i.e., that it is variadic, that the binary case of this operation is associative, that applying it to more than two arguments can be restated as repeated application of the binary form, and also that the unary and nullary cases of the operation follow suit. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + The claim that the arith1#plus operation is n-associative: + + + + + + + + + This file was generated from list4u.tex. + +