Language syntax

Grim has a single data structure: symbolic expression trees. A Grim expression is either of the following:

Example

An entry in Fungrim is represented by a single Grim expression that contains various metadata as well as the main formula as subexpressions. For example:

Entry(ID("22dc6e"),
    Formula(Equal(Fibonacci(n), Add(Fibonacci(Sub(n, 1)), Fibonacci(Sub(n, 2))))),
    Variables(n),
    Assumptions(Element(n, ZZ)))

The formula is the recurrence relation for Fibonacci numbers: $F_{n} = F_{n - 1} + F_{n - 2}$. The metadata in this case specifies the Fungrim entry ID (22dc6e, as a string), lists the free variables in the formula (here the single variable n), and provides conditions on the variables ("assumptions"), in this case $n \in \mathbb{Z}$, such that the formula represents a theorem.

Some points of caution

String representation and infix operators

Every Grim expression has a canonical string representation, for example Add(3, Mul(-5, x)). The simple syntax ensures that Grim expressions are syntactically valid in common programming languages. Pygrim simply embeds Grim as a domain-specific language within Python, using Python's native integer literals and function call syntax (the necessary symbols have to be created as Python variables).

Because function-call syntax is clumsy for complex arithmetic expressions, we frequently write Grim expressions in an extended syntactical form using infix arithmetic operators (+, -, *, /, **) as well as parentheses for grouping and with use of parentheses and brackets for tuples and lists. Pygrim supports this syntax by overloading the Python-level arithmetic operators (with the operator precedence rules of Python). We need to be careful: for example, we can do x / 3 to construct the Grim expression Div(x, 3) in Python when x is a Grim symbol, but 1 / 3 in Python does not give Div(1, 3).

Symbols available for variables

Symbols reserved for builtin objects (such as Add and ZZ) start with an uppercase letter and are at least two characters long, so all single-letter symbols and all symbols beginning with a lowercase character can be used for variables.

Most Greek letter names are available as symbols and are recognized by the LaTeX converter. There are some exceptions: Gamma is reserved for the gamma function, and Pi is reserved for the constant π; one should use GreekGamma and GreekPi for the Greek capital letters as variables. The alternative spelling lamda / Lamda is used for "lambda" since lambda is a reserved keyword in Python.

As a convenience hack: a symbol name ending with an underscore results in function calls being rendered as subscripts (but watch out as a_ is not the same symbol as a, and the symbols are not implicitly connected.

Input: Set(a, b, c, d, e, f, g, h, i, j, k, l, ell, m, n, o, p, q, r, s, t, u, v, w, x, y, z)
$$\left\{a, b, c, d, e, f, g, h, i, j, k, l, \ell, m, n, o, p, q, r, s, t, u, v, w, x, y, z\right\}$$

Python variables predefined in Pygrim.

Input: Set(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z)
$$\left\{A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z\right\}$$

Python variables predefined in Pygrim.

Input: Set(alpha, beta, gamma, delta, epsilon, zeta, eta, theta, iota, kappa, lamda, mu, nu, xi, pi, rho, sigma, tau, phi, chi, psi, omega)
$$\left\{\alpha, \beta, \gamma, \delta, \varepsilon, \zeta, \eta, \theta, \iota, \kappa, \lambda, \mu, \nu, \xi, \pi, \rho, \sigma, \tau, \phi, \chi, \psi, \omega\right\}$$

Python variables predefined in Pygrim.

Input: Set(Alpha, Beta, GreekGamma, Delta, Epsilon, Zeta, Eta, Theta, Iota, Kappa, Lamda, Mu, Nu, Xi, GreekPi, Rho, Sigma, Tau, Phi, Chi, Psi, Omega)
$$\left\{\Alpha, \Beta, \Gamma, \Delta, \Epsilon, \Zeta, \Eta, \Theta, \Iota, \Kappa, \Lambda, \Mu, \Nu, \Xi, \Pi, \Rho, \Sigma, \Tau, \Phi, \Chi, \Psi, \Omega\right\}$$

Python variables predefined in Pygrim.

Input: Tuple(f(n), a_(n), gamma_(m,n), f_(n)(x))
$$\left(f(n), a_{n}, \gamma_{m, n}, f_{n}(x)\right)$$

Function calls.

Last updated: 2020-03-06 00:22:16