How it started?

• With the webALT project:

• Aiming at providing a multilingual repository of simple math exercises for secondary education.

• GF the chosen tool
  • Not mature enough at that time
  • Finnish took hours to compile

The Grammatical Framework: GF

GF logo

• Language for developing grammars
  • BNF, yacc, etc.
• Functional language
  • lisp, haskell, etc.
• Natural language processing framework
  • based on type theory

The Mathematics Grammar Library

• Basic math objects from some Content Dictionaries.

• 15 languages so far: mathbar

• Available at svn://molto-project.eu/mgl

The Mathematics Grammar Library

mgl structure

Other upper layers

Operations

Simple drills.

Commands

Queries/Answers to/from a CAS.

WordProblems

Modeling and solving simple word problems.

Some examples

• At OpenMath level:

    abs : ValNum -> ValNum ;            -- the absolute value of z
    times : [ValNum] -> ValNum ;        -- the product of x, y and z
    unary_minus : ValNum -> ValNum ;    -- minus x

• At Commands level:

  Compute  :  (k: Kind) -> Value k -> Command ;          
  Assign   :   (k: Kind) -> Variable k -> Value k -> Command ; 
  Assert   : Prop -> Command ;
  Approximate  : ValNum -> Command ; 
  BeginBlock  : String -> Command ;
  EndBlock    : String -> Command ; 

Abstract/Concrete types

• Values:
  • ValNum, ValSet, ValTensor ... = MathObj = Noun Phrase (NP)
  • ValFun = MathFunc = NP + Extra info
• Variables:
  • VarNum, VarSet, ... = Symbol (= String in most languages)
• Propositions:
• Prop = Clause with polarity
• FullProp = Sentence
• Clauses can be converted into Questions (not the case with Sentences).

A simple example

• The absolute value in Arith1:

    abs : ValNum -> ValNum

• At concrete level:

    abs : NP -> NP

Concrete differences

  value_N : N       = mkN "value"  ;
  absolute_A : A    = mkA "absolute"  ;                       -- In LexiconEng
  abs_value_CN : CN = mkCN absolute_A value_N ;              -- In LexiconX
  
  mkNP the_Art (mkCN abs_value_CN (mkAdv possess_Prep obj)) ; -- In Arith1I

1. In English: Combine the adjective "absolute" with the noun "value" to get a common noun (CN)

2. Combine this with the argument (NP) using the "of" preposition. It gives a CN;

3. Combine this with a determiner ("the") to give an NP.

In German:

  absolute_A : A    = mkA "absolut"  ;
  value_N : N       = mkN "Wert" "Werte" masculine  ;         -- In LexiconGer
  abs_value_CN : CN = mkCN absolute_A value_N ;              -- In LexiconX
  
  mkNP the_Art (mkCN abs_value_CN (mkAdv possess_Prep obj)) ; -- In Arith1I

Associative operators

    plus : [ValNum] -> ValNum

    plus : ListNP -> NP

DefGenCN sum_CN (mkNP and_Conj terms)

• Lists are formed by prepending an object to an existing list (ConsNP).

• Minimal list: BaseNP x y
  • The number of elements in the base case can be set for each category
  • It is 2 in the case of [ValNum]

1. ListNP is basically a list of NP which knows if there is 2 or more elements in it:
   • "the sum of x and y": BaseValNum x y
   • "the sum of x, y and z": ConsValNum x (BaseValNum y z)

2. We combine ListNP with the "and" conjunction to get a new NP

3. As in the previous example: combine with "sum", etc.

The case of functions

MathFunc = Kind + Variable + NP

Named function

"the cosine of 3"

Function variable

"f at 3"

General case

"the derivative of the sine at 3"

Lambda abstraction

"x to the cosine of x where x is 3"

The importance of transfers

"Compute the integral of the function mapping x to the square of x from minus infinity to infinity."

Compute Num (fromNum (
  defint_interval (lambda x (power2 (Var2Num x))) nums1_minus_infinity nums1_infinity))

Compute Num (fromNum (
  defint_interval (lambda x (power2 (Var2Num x))) (unary_minus nums1_infinity) nums1_infinity))

• It is ambiguous (not really)

• power2 must be power (int2num 2)
• (unary_minus nums1_infinity) must be nums1_minus_infinity (maybe?)
• defint_interval must be defint on interval_cc:
  • "compute the integral of the function mapping x to the square of x on the closed interval from minus infinity to infinity."

Transfers

• Modifying the abstract tree.

• GF is very limited on this (def judgments).

• Use the GF bindings to other languages
  • haskell, python, javascript, C runtime

Concluding remarks

• The mgl GF library provides parsing/linearizing between 15 natural languages and an abstract representation similar to OpenMath. Tested for 3 languages.

• Developing a new language L:
  • Resource Grammar support
  • Fill LexiconL
  • Review cycle
• Developing a new module M:
  • Add abstract module M
  • Add entries to LexiconX to support M
  • Add concrete modules for M
  • Input from language + maths experts
  • Review cycle