Scala is a general purpose programming language that includes a read-eval-print loop (REPL). Mmt is a general representation language for formal mathematical knowledge implemented in Scala. Independent recent developments permit combining them into an extremely simple user interface that can act as a nucleus for a variety of systems. Firstly, Scala introduced string interpolation { a convenient syntax that permits escaping back and forth between strings and arbitrary Scala expressions (while preserving type safety). Secondly, Mmt introduced a notation-based text syntax and a rule-based evaluation engine for its mathematical objects (which are based on OpenMath). Combining these, users can enter and work with Mmt objects in the Scala-REPL with so little overhead that it essentially behaves like a dedicated Mmt-REPL { except for also providing the full power of Scala. Implicit conversions (e.g., between integers represented in Mmt and Scala integers) further blur the distinction between meta- and object language. Mmt is highly extensible: Users can add new type systems and logics as well as new theories and notations and evaluation rules. Thus, we obtain a REPL-style interface for any language represented in Mmt with essentially no e ort.
Declaring Symbols A theory declaration T = fSym g introduces a theory with name T containing a list of symbol declarations. A symbol declaration c : ! = !0 # introduces a symbol named c with type !, de niens !0 and notation (all of which are optional).
Terms ! over a theory T are formed from symbols OMS(T ?c) declared in T , bound variables OMV(x), applications OMA(!; !1; : : : ; !n) of a function ! to a sequence of arguments, bindings OMBIND(!; X; !0) using a binder !, a bound variable context X, and a scope !0 as well as integers OMI(i) and oats OMF(f ) where i and f are integers and oats, respectively. This is a fragment of the OpenMath language [BCC+04].
Remark 1. For readability we will write T ?c instead of OMS(T ?c) in the following. Furthermore, we will write c instead of T ?c when the theory T is clear from the context.
Example 1. Figure 1 shows an Mmt theory Lists, based on the logical framework LF [HHP93]. Lists declares natural numbers and lists as well as additional operations on them (plus for naturals and append for lists). Using the Mmt notation language, described below, we also declare the usual notations: in x + , :: and ::: for plus, cons, and append, respectively. theory Lists meta LF tp : type tm : tp ! type # tm A1 nat : tp zero : tm nat # o succ : tm nat ! tm nat # s A1 plus : tm nat ! tm nat ! tm nat # A1 + A2 list : tp ! tm nat ! tp # list A1 A2 nil : fAg tm list A zero cons : fA; N g tm A ! tm list A N ! tm list A (s N )
# A3 :: A4 append : fA; M; N g tm list A M ! tm list A M ! tm list A (M + N ) # A4 ::: A5 Remark 2. The theory Lists from Figure 1 has the theory LF as meta-theory which means that all symbols and notations declared in LF are available and can be used in Lists.
Speci cally, in Lists, we use the symbols for type, arrow (with notation A1 ! A2), and the Pi binder (with notation f V1 g S2) all of which are declared in LF with the corresponding notations.
Adding Notations Notations act as the parsing and printing rules that transform between abstract syntax and text-based concrete syntax (that supports Unicode). A notation is a sequence of notation elements which can be either delimiters (i.e. strings), argument markers (An), variables Vn and scopes Sn where n is a number representing an argument position in the abstract syntax. Variables and scopes are in principle used for binders (e.g. the Pi binder in LF ), and the majority of symbol notations only need delimiters and arguments. For example, the notation for in x addition is given as A1 + A2. It implies that conjunction is binary and constructs the application object.
It is typical to omit arguments if their value can be inferred from the remaining arguments. We call this implicit arguments. Therefore, we introduce a simple convention: if a component number n is absent in a notation but a higher number is present, then the missing component is assumed to be an implicit argument An. For instance, we use the notation A3 :: A4 for cons above meaning that the rst two arguments (the contained type A and the size N ) are implicit.
We omit here the details regarding the parsing algorithm and only point out that our notation language is more complex and also covers sequence arguments. Furthermore, notations technically also include an integer precedence, which is used to resolve ambiguities when multiple notations are applicable. Adding Evaluation Rules Mmt allows users to declare evaluation rules for each symbol [KMR13]. Intuitively, the evaluation rule of a symbol c acts as the implementation of the computational semantics of c.
We give evaluation rules for plus and append, declared above in theory Lists. For example, the rule for plus is declared as an Mmt assignment which maps plus to a -expression ( together with its notation "=>" are declared in the ScalaOM meta-theory). The -expression maps the arguments x; y of plus to a Scala code snippet written between Mmt escape characters (shown here as quotes).
A module within the Mmt-API, called the Universal OpenMath Machine (UOM), translates the theory and the view to a Scala object and trait, respectively. Each Mmt constant (e.g. plus) is translated to a Scala object which acts as the Scala constructor and pattern matcher for that constant. As a result, instead of writing e.g. OM A(OM S("plus"); a; b) we can directly write plus(a; b) to construct an Mmt term in Scala. Furthermore, the UOM translates each expression vars => snippet to a function whose arguments are vars and whose body is snippet. These functions are stored by the UOM in a rule store S. When given an expression E, the UOM exhaustively applies the rules in S on E. Example 2 (Continuing Example 1). We give evaluation rules for plus and append, declared above in theory Lists. The rules are declared as Mmt assignments which map plus and append to Scala code snippets.
Given the evaluation rules from Figure 2, we can use the UOM to evaluate OMA(plus; OMA(succ; zero); OMA(succ; OMA(succ; zero))) and reduce it to OMA(succ; OMA(succ; OMA(succ; zero))) (i.e. in decimal notation 1 + 2 to 3 ). view Impl : Lists ! ScalaOM = plus = (x : Term; y : Term) => "scala y match f case zero => x case succ(z) => succ(plus(x, z)) case => plus(x, y) " " g g append = (a : Term; m : Term; n : Term; ls1 : Term; ls2 : Term) "scala ls1 match f case nil => ls2 case cons(a, n, h, t) => cons(a, n, h, append(a, m, n, t, ls2)) case => append(a, m, n, ls1, ls2) Scala [OSV07] is a programming language that integrates the functional and object-oriented paradigms. It compiles to Java bytecode and can be seamlessly integrated with existing Java libraries. Scala also includes a read-eval-print loop for interactive evaluation of expressions.
Scala recently introduced processed strings [Ode12] as a generalization of string literals. A processed string consists of an identi er followed by a string literal within which two forms of escaping are valid: (i) $var for individual variables and (ii) $f expr g for complex expressions where $var is syntactic sugar for $f var g.
Thus, a processed string is of the form: id"text0 $f expr1 g text1 $f exprn g textn " where id de nes the interpolation function that processes the string.
Besides a few built-in interpolation functions, Scala permits users to declare arbitrary custom interpolation functions id. These must take as arguments a sequence of strings (the parts texti) and a sequence of typed expressions (the expressions expri). String interpolation is type-safe: the argument types of id de ne what expressions expri are legal. 3
Interpolating MMT Expression We implemented two string processors for Mmt terms. This allows us to combine and nest Mmt and Scala expressions and use Mmt-speci c services directly from the Scala shell.
(i) mmt, which calls the Mmt parser to evaluate an interpolated string literal into an Mmt object and (ii) uom, which uses mmt but additionally calls the UOM simpli er to perform computation on the resulting term. mmt takes a sequence of strings texti and a sequence of Mmt-terms termi. It concatenates the strings texti and inserts a fresh free variable xi for every termi. The resulting string is parsed into an Mmt term as usual, and afterwards each xi is substituted with termi.
For example, if the Scala variables a and b hold the Mmt-terms OMI(3) and OMI(5), respectively, then mmt"$a + + $b" is interpolated to the Mmtterm OMA(plus; OMI(3); ; OMI(5)). And, given appropriate evaluation rules as described in [KMR13], uom"$a + + $b" yields OMA(plus; OMI(8); ).
We can also escape back and forth between Scala and Mmt. For example, if substitute(t; n; s) is the Mmt-function for substituting the variable named n in the term t with s, then
mmt" + $fsubstitute(mmt"x + x"; "x"; a)g" yields OMA(plus; ; OMI(3); OMI(3)) by parsing the string then substituting "x" with a and a with its value OMI(3) in the resulting term.
In general, this has the e ect that mmt":::" escapes from Scala into Mmt, and $f:::g escapes from Mmt into Scala.
An MMT-REPL Based on the string processors described above we can use Mmt and the UOM directly in the Scala shell and to nest and combine Mmt terms and Scala expressions.
Example 3 (Continuing Examples 1 and 2). Using the uom interpolator we can integrate Mmt notations and evaluation rules inside the Scala environment. For instance, in the example below we use the notations and evaluation rules for symbols plus and append to perform operations on Mmt terms from the Scala REPL. 1 > uom"s o + s (s o)" 2 s (s (s o)). 3 > uom"(o :: (s o) :: nil) ::: (o :: nil)" 4 (o :: (s o) :: o :: nil).
Note that, in the listing above, we show the result using Mmt notations (and not the abstract syntax) for readability but, technically, it now also contains the inferred values for the implicit types and arguments. For example, the subterm o :: nil from the list above corresponds to OMA(cons; nat; zero; zero; nil) in abstract syntax. Furthermore, its type is inferred as OMA(list; nat; OMA(succ; zero)) (i.e. list of type nat and length 1)
While notations do increase usability and readability, unary natural numbers remain awkward to work with. But we also allow users to directly write numbers in Mmt concrete syntax. They are automatically parsed into the OpenMath counterparts: OMI for integers and OMF for oats.
Example 4. linalg2 ?vector refers to an Mmt declaration that implements the OpenMath symbol for vectors. It also has the notation h SA i where h and i are delimiters and SA is a sequence argument representing an arbitrary number of arguments from the abstract syntax (comma separated). Therefore, we can use the notation to construct vectors of integers and the UOM to perform computations on them (the evaluation rules for addition of OpenMath integers, oats and vectors are already implemented [KMR13]). 1 > mmt"h1,2,3i" 2 OMA(linalg2 ?vector ; OMI(1); OMI(2); OMI(3)) 3 > uom"h1,2,3i + h2,3,4i" 4 OMA(linalg2 ?vector ; OMI(3); OMI(5); OMI(7))
Implicit Conversions Furthermore, we use Scala implicit conversions to automatically convert Scala terms to corresponding Mmt terms (e.g from Scala integers to Mmt/OpenMath integers).
Example 5. After implementing the following implicit conversion from Scala integers to Mmt/OpenMath integers:
implicit def int2OM(i: Int) = OMI(i) we can interpolate Scala integers into Mmt-speci c string literals. 1 > var x = 3 2 > mmt"$x + ${4 - 2}" 3 OMA(arith1 ?plus; OMI(3); OMI(2)) 4 > uom"$x + ${4 - 2}" 5 OMI(5)
Moreover, we can use implicit conversions in the opposite direction to be able to use the result of computations performed by Mmt and the UOM in Scala. Example 6. After implementing the implicit conversion from Mmt/OpenMath to Scala integers we can use directly use them inside Scala expressions. In the example below, and are Scala operators, + is the notation of the Mmt symbol plus and the nal result is a Scala integer. 1 > 7 * uom"$x + ${4 - 2}" 2 35
Implicit conversion also works for more complex notions as long as there is a Scala counterpart. Moreover, since the UOM automatically constructs Scala objects for each Mmt symbol declaration, we can easily refer to and construct Mmt objects from within Scala.
Example 7. For instance, we can de ne implicit conversions between Mmt and Scala vectors. In the listing below, Scala automatically converts the Mmt term vect into a Scala vector and then during the map operation, each Mmt integer into the corresponding Scala integer nally yielding a Scala vector as a result. 1 > var vect = uom"vector 1 2 3" 2 OMA(linalg2 ?vector ; OMI(1); OMI(2); OMI(3)) 3 > vect.map(x => 1 + x)} 4 Vector(2, 3, 4) Applications Even though we only gave simple, self-contained examples here, the Mmt interpolator can serve as the kernel of a wide variety of services. For example, any Scala or Java library can be integrated directly to carry out computations or to pre- or postprocess values. Moreover, with implicit conversions between Scala and Mmt objects this integration can be done seamlessly and with little overhead. This design corresponds to how the Sage computer algebra system [S+13] is built on top of the Python interpreter. For example, semantic services (type inference, presentation, de nition lookup, etc.) implemented in Mmt can be immediately used for the resulting terms.
Alternatively, the Mmt interpolator can be used a subsidiary component. For example it is straightforward to give a web interface for the interpolator where the user enters terms in text syntax and the system dynamically displays the presentation MathML rendering of the input term and its simpli cation result.
At the same time, because computation is implemented using evaluation rules, it is easy to support step-wise computations. This permits applications such as an interactive E-learning system that lets users choose simpli cation rules from a set of applicable rules. In the same way, interactive theorem proving can be seen as the step-wise application of computation steps, in this case computing new goals from the given one. 4
The combination of the Mmt notation language and Scala string interpolation yields an input language for mathematical objects that permits arbitrary escaping between Scala and Mmt. This turns the Scala REPL into an Mmt-REPL that gives users access to notations and computation rules de ned in Mmt, the syntax manipulation functions de ned in the Mmt API, and any custom function de ned in arbitrary Java/Scala packages.
Clearly, this Scala/MMT-REPL does not give us a powerful computer algebra system. But, it is interesting to consider what is missing. Indeed, we can easily imagine building a CAS on top of the Mmt REPL by adding symbols, notations, and evaluation rules. This has the appeal that users can write mathematical algorithms using a strongly typed and widely used general purpose programming language. Existing CASs can be integrated by simply treating each CAS as a separate simpli cation rule that can be called on demand.
In the long run, Mmt can serve as a formalization language, in which the axiomatic structure of the mathematical theories is described. This can serve as a documentation and interoperability layer. For example, we envision that Mmt transforms a formal theory structure into class diagrams in various programming language. These generated classes would provide interfaces that CASs can implement to make them interoperable. It also becomes possible to generate test cases from axioms.