10Handling Mathematical Expression Data

This chapter introduces Egison's features for handling symbolic computation.

10.1Internal Representation of Mathematical Expression Data

Mathematical expressions are directly implemented as a built-in data type within the Egison interpreter using Haskell data types. This section explains the internal data structure that represents mathematical expression data.

Mathematical expression data is represented as a fraction that takes polynomials in sum-of-products normal form for both the numerator and denominator. Therefore, for example, the result of adding two fractions whose denominators are polynomials is combined into a single fraction over the common denominator.

declare symbol x, y, a, b, c

a / (b + 1) + x / (y + 1)
-- (b x + a y + x + a) / (b y + y + b + 1)

A polynomial is represented as data consisting of a list of terms. A term is represented as data consisting of a coefficient and an association list of factors and exponents. For example, the term 3 * x^2 * sqrt 2 has 3 as the coefficient and [(x, 2), (sqrt 2, 1)] as the association list. Exponents can also be negative integers. That is, polynomials in Egison are Laurent polynomials. A fraction whose denominator consists of a single term is not kept as a fraction; it is folded into the terms using negative exponents.

a / b + x / y -- x y^-1 + a b^-1

Besides symbols, factors can be the symbolic function applications introduced in Section 9.2, the quoted expressions introduced in Section 10.2, and the function symbols explained in Chapter 13. A symbol consists of its name string and a list of indices. Indices are explained in Chapter 12, which covers tensors.

This internal structure can be decomposed by pattern matching with the mathValue matcher defined in the Egison library. For example, a polynomial can be decomposed into its list of terms.

match (x - sqrt 2) as mathValue with
  | poly $ts -> ts
-- [x, - 'sqrt 2]

Patterns for mathematical expressions are introduced in detail in Section 10.6. Furthermore, the same mathematical expression can be represented by several different internal structures (for example, a flat polynomial and a nested polynomial), and the structure can be selected with type annotations. This is explained in Chapter 11.

Numbers are a complex data type. Up to natural numbers, they can be elegantly defined as algebraic data types. However, when considering subtraction, the inverse of addition over natural numbers, the concept of negative numbers emerges. Furthermore, considering the inverse of multiplication, which is obtained by repeated addition, leads to the concept of rational numbers. Moreover, considering the inverse of exponentiation, which is obtained by repeated multiplication, leads to the concepts of square roots, imaginary numbers, and algebraic numbers that include them.

10.2Controlling Expression Expansion with Backquotes (`)

As mentioned in Section 9.1, Egison automatically expands mathematical expressions into sum-of-products normal form, but this expansion can be controlled using backquotes (`). An expression following a backquote is treated like a single symbol.

`(x + 1)^2
--  `(x + 1)^2

`(x + 1) + `(x + 1)
--  2 * `(x + 1)

`(x + 1) + (x + 1)
-- x + `(x + 1) + 1

Backquotes are useful when we do not want expressions to be expanded. Reduction of polynomial fractions itself is performed automatically by polynomial GCD, as mentioned in Section 9.3, but both the input and the result are expanded into sum-of-products normal form.

(x + 1)^2 / (x + 1) -- x + 1
(x^2 - y^2) / (x - y) -- y + x

If the factored form is preserved using backquotes, the expression is reduced without going through expansion, and the result is also obtained in factored form.

`(x + y)^2 / `(x + y) -- `(y + x)
`(x - y) * `(x + y) / `(x - y) -- `(y + x)

An expression quoted with a backquote is treated as a factor, on the same footing as a symbol, within Egison's internal mathematical expression data. This is why `(x + 1)^2 above is kept as a power of a single factor without being expanded.

10.3Controlling Function Application with Single Quotes (')

For applications of defined functions, we sometimes want to return a symbolic result without evaluating the function application. For example, we want the sqrt function to behave as follows, as we saw in Section 9.2.

declare symbol x, a

sqrt 4 -- 2
sqrt x -- 'sqrt x

To realize this behavior, Egison provides single quotes (') as a built-in syntax. A single quote is followed by a function, and even if that function is defined, the application is returned as a symbolic function application without being evaluated.

def f (x: MathValue) : MathValue := x + 1

f a -- a + 1
'f a -- 'f a

Symbolic function applications are also displayed with a leading single quote in the output. Single quotes are used in the bodies of the declare apply statements introduced in Section 11.3 — for example in the definitions of sqrt and the trigonometric functions sin and cos — to return symbolic values for inputs that cannot be simplified further.

10.4Suppressing Rule Application with '( )

Prefixing a parenthesized expression with a single quote builds the expression without applying the rewrite rules declared with declare rule (Section 11.1 of Chapter 11). Structural normalization — expansion into sum-of-products normal form and merging of like terms — still happens.

declare symbol x, `$\theta$`

w^2 + w + 1 -- 0
'(w^2 + w + 1) -- w^2 + w + 1

(sin `$\theta$`)^2 + (cos `$\theta$`)^2 - 1 -- 0
'((sin `$\theta$`)^2 + (cos `$\theta$`)^2 - 1) -- 'sin `$\theta$`^2 + 'cos `$\theta$`^2 - 1

'(2 * x + x) -- 3 * x
'((x + 1)^2) -- x^2 + 2 * x + 1

The typical situation that needs this quote is treating a relation that is itself subject to simplification rules as data. For example, when passing ideal generators to polyNF (Section 11.2 of Chapter 11), writing the Pythagorean relation plainly would let the existing auto rules collapse it to 0 at construction time. Wrapped in '( ), the relation survives as an expression.

This completes the set of three quotes. The backquote ` freezes an expression into a single atom and stops expansion (Section 10.2), the single quote 'f stops the evaluation of a function application (Section 10.3), and '( ) stops the application of rewrite rules. Each quote freezes a different layer: the structure of an expression, function application, and the equational theory.

10.5Declaring Local Symbols with withSymbols Expressions

Symbols declared with the declare symbol statement are global. For cases where symbols are needed only temporarily, Egison provides the withSymbols expression, a syntax for declaring local symbols. The withSymbols expression takes a list of variables as its first argument, and these variables are treated as symbols during the evaluation of the expression in the second argument. Even if a variable is already defined, it is treated as a symbol inside the withSymbols expression.

def k : Integer := 10

k -- 10
withSymbols [k] k -- k
k + withSymbols [k] k -- k + 10

Local symbols declared with a withSymbols expression are processed as symbols independent of the global symbols declared with the declare symbol statement. The two js below are displayed with the same name, but since they are different symbols, they are not combined into 2 * j.

declare symbol j

j + withSymbols [j] j -- j + j

10.6Pattern Matching on Mathematical Expression Data

This section introduces the patterns provided for mathematical expression data. The matcher mathValue for mathematical expressions is implemented in the Egison library. The definition of mathValue can be found in lib/math/expression.egi. In addition, several syntactic sugars are built in for writing patterns for mathematical expressions in a form closer to mathematical notation. This section also introduces these syntactic sugars. Pattern matching on mathematical expressions is demonstrated in Section 9.5. Please refer to the program in Section 9.5 for concrete examples of using these patterns.

10.6.1Pattern Matching on Factors

The pattern constructors for factors are symbol, apply1 through apply4, quote, and func. symbol pattern-matches symbols; apply1 through apply4 pattern-match the symbolic function applications introduced in Section 9.2; quote pattern-matches backquoted expressions introduced in Section 10.2; and func pattern-matches objects called function symbols, explained in Chapter 13.

The first argument of the symbol pattern constructor pattern-matches the name string of the symbol, and the second argument pattern-matches the list of indices. Indices are covered again in Chapter 12, which explains tensors.

match x as mathValue with
  | symbol $s _ -> s
-- "x"

Although symbols can be pattern-matched using the symbol pattern constructor, in practice, value patterns are more commonly used.

match x as mathValue with
  | #x -> "Matched"
  | _ -> "Not matched"
-- "Matched"

For symbolic function applications, the pattern constructors apply1 through apply4 are used according to the number of arguments. The first argument pattern-matches the function itself, and the remaining arguments pattern-match the expressions of the respective arguments. For the function itself, value patterns such as #sqrt are commonly used.

match (sqrt x) as mathValue with
  | apply1 #sqrt $g -> g
-- x

The quote pattern constructor takes a pattern for mathematical expressions as its argument. This pattern is matched against the expression inside the quote using the mathValue matcher.

match `(x + 1) as mathValue with
  | quote $e -> e
-- x + 1

10.6.2Pattern Matching on Terms

The term pattern constructor is used for pattern matching on terms. The first argument of the term pattern constructor pattern-matches the coefficient, and the second argument pattern-matches the association list of factors and exponents. The assocMultiset matcher introduced in Section 6.7 is used for pattern matching the association list of factors.

matchAll 3 * x^2 * y as mathValue with
  | term $a (($x, $n) :: $xs) -> (a, x, n, xs)
-- [(3, x, 2, [(y, 1)]), (3, y, 1, [(x, 2)])]

The term pattern constructor has syntactic sugar for writing patterns in a form closer to mathematical notation. In the first pattern below, $x matches a factor together with its power, such as x^2, and $xs matches the product of the remaining factors. As in the second pattern, a pattern for the exponent can also be written following ^.

matchAll 3 * x^2 * y as mathValue with
  | $a * $x * $xs -> (a, x, xs)
-- [(3, x^2, y), (3, y, x^2)]

matchAll 3 * x^2 * y as mathValue with
  | $a * $x^#2 * $xs -> (a, x, xs)
-- [(3, x, y)]

10.6.3Pattern Matching on Polynomials

The poly pattern constructor is used for pattern matching on polynomials. The poly pattern constructor takes a pattern that matches a list of terms as its argument.

matchAll x + y + 1 as mathValue with
  | poly ($x :: $xs) -> (x, xs)
-- [(y, [x, 1]), (x, [y, 1]), (1, [y, x])]

The poly pattern constructor also has syntactic sugar for writing patterns in a form closer to mathematical notation.

matchAll x + y + 1 as mathValue with
  | $x + $xs -> (x, xs)
-- [(y, x + 1), (x, y + 1), (1, y + x)]

10.6.4Pattern Matching on Rational Expressions

The frac pattern constructor is used for pattern matching on rational expressions. The first argument of the frac pattern constructor pattern-matches the numerator polynomial, and the second argument pattern-matches the denominator polynomial.

matchAll (a + b) / (c + 1) as mathValue with
  | frac $x $y -> (x, y)
-- [(b + a, c + 1)]

Note that, as mentioned in Section 10.1, a fraction whose denominator consists of a single term is represented as a term with negative exponents, and hence does not match the frac pattern.

The frac pattern constructor also has syntactic sugar for writing patterns in a form closer to mathematical notation.

matchAll (a + b) / (c + 1) as mathValue with
  | $x / $y -> (x, y)
-- [(b + a, c + 1)]