• A prototype from MOLTO.

  • Mathematical Grammar Library
  • 2 gf pathways: NL to Sage, Sage to NL.

• With the webALT project:

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

• GF the chosen tool

• Basic math objects from some OpenMath Content Dictionaries.

  • Small Type System: Base for the GF abstract module

• 15 languages so far: mathbar

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

The library is organized in 3 layers of increasing complexity:

• Ground: For literal integers and variables
• OpenMath: For OpenMath objects
• Operations: Problems, verbalizations, ...

• Operations: Simple drills.

• Commands: Queries/Answers to/from a Computer Algebra System.

• Word Problems: Modeling and solving simple word problems.

• 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 ;
  

Goal: Dependent types all the way down.

• Values:

  • ValNum, ValSet, ValTensor ... = Noun Phrase (NP)
  • ValFun = MathFunc = NP + Extra info

• Variables:

  • VarNum, VarSet, ... = Symbol

Goal: Value Number, Variable Number, ...

• In English:

  oper abs_value_CN : CN = mkCN absolute_A value_N ;     -- In LexiconEng
  lin abs obj =
    mkNP the_Art
       (mkCN abs_value_CN (mkAdv possess_Prep obj)) ;  -- In Arith1I
  
   unary_minus ob = mkNP (mkCN minus_N ob) ;
  

• In Finnish:

  unary_minus x = mkNP (E.GenNP x) (mkN "vastaluku") ;
  

• In Sage:

  unary_minus x = mkPrec 1 ("-" ++ (usePrec 3 x));
  

fun plus : [ValNum] -> ValNum

lin plus : ListNP -> NP

DefGenCN sum_CN (mkNP and_Conj terms)

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

• 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)

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

oper
   MathFunc = {t:FuncForm; s2:MathVar} ** NP ;
param
  FuncForm = FNoVar | FNamed | FVar | FGral ;

• 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"

• Most of the productions have a verbal/formula rendering

  • Arith1Eng
  • Arith1LaTeX

• Goal: To combine them:

The square root of \( x^2 + 1\)

number_typed : VarNum -> QVarNum ;
number_list  : [VarNum] -> QVarNum ;
number_range : VarNum -> VarNum -> QVarNum ;

\(n\) "number"

\(x\), \(y\) and \(z\) "prime numbers"

\(x_1,\dots,x_n\) "natural numbers"

q_natural,
q_integer,
q_rational,
q_even,
q_prime : QVarNum -> QVarNum ;

"Let \(x_1,\dots,x_n\) be natural numbers, ..."

Prop   = S
[Prop] = [S]
SimpleProp = MathCl = Cl ** {p:Polarity}
QProp = QS ;

Prop = MathCl = Cl ** {p:Polarity}
[Prop] = [MathCl]
Prop --> S, QS

7 is prime.

is 7 prime?

[Prop] --> S, QS

7 is prime and 8 is not prime.

is it true that 7 is prime and 8 is not prime?

"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 --> power (int2num 2)

• (unary_minus nums1_infinity) --> nums1_minus_infinity

• Modifying the abstract tree.

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

• Use the GF bindings to other languages

  • haskell
  • python,

cat
  Kind ;
  Command;
  Answer;
  Value Kind;
  Variable Kind ;

fun
  Num, Fun, Set, Tensor : Kind ;

data Compute :  (k: Kind) -> Value k -> Command ;

fun
  addTo : ValNum -> ValNum -> Command ;

  itNum   : ValNum ;
  itSet   : ValSet ;

  Simple :   (k: Kind) -> Value k -> Answer ;
  FeedBack : (k: Kind) -> Value k -> Value k -> Answer;

def
  addTo x y          = Compute Num (fromNum (plus (BaseValNum x y))) ;
  bracket_emptyset = Simple Set (fromSet emptyset) ; -- {}

def
  bin_over x y = divide x y ;
fun
  isEqual   : (k: Kind) -> Value k -> Value k-> Command ;
  isAppEqual: (k: Kind) -> Value k -> Value k-> Command ;

  Yes: Answer ;
  No: Answer ;
  YesApprox: Index -> Answer ;

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

  • Tested for 3 languages.

• It can be used to interact with mathematical software using natural language.

1. Resource Grammar support
2. Fill LexiconL
3. Review cycle
   • Fix idiomatic productions

1. Add abstract module M
2. Add entries to LexiconL to support M
3. Add concrete modules for M
4. Review cycle:
   • Input from language + maths experts

• Dependent types

• Reduce indirection and simplify module structure

• Mixtures

• Qualified variables