User:Realazthat/Projects wishlist/MathML2X

Write an XSLT transform to convert a function written in a subset of MathML to <some language>. This will allow one to specify an algorithm mathematically and not worry about the programming details, while a programmer can use the algorithm without knowing the math behind it. It also allows one to specify the algorithm in the universal language of math. Many algorithms are best described in different types of math, and MathML can be used to semantically express these algorithms. In particular, I find many functions I write easily expressible in discrete math, and would love to do just that, and generate the code automatically.

Features

• Ability to store algorithms as calculus+set theory etc., and realize that to code, both in arbitrary precision, or, depending on input constraints to native types etc
  • A generic (arbitrary type) algorithm to code converter
  • Arbitrary precision
  • Ability to limit precision for transformation, so that generated code uses native types
• Program in LaTeX

Languages

Possible backend languages:

Imperative:

• HLML

Declarative:

• wp:Epigram_(programming_language)

  Would be really cool; it isn't Turing complete (not everything would be expressable then; no unbounded loops)

• SMT-LIB for use with an SMT solver

  It would making writing constraints easier

• {Other declarative language here}
• Haskell | Scheme | Prolog
• wikipedia:Constraint_programming

Examples

These aren't concrete, as my ideas of how things *should* work are not concrete.

Factorial

$f(n\in \mathbb {N} )\in \mathbb {N} ={\begin{cases}1&{\text{if }}n=0\\f(n-1)\cdot n&{\text{if }}n>0\end{cases}}$

$\mathbb {N}$ can be mapped to arbitrary precision numbers, or the native (unsigned?) integer etc. This function would be implemented with recursion.

Another way of expressing factorial:

$f(n\in \mathbb {N} )\in \mathbb {N} =\prod _{k=1}^{n}k$

Notes:

• The types here are implicit, perhaps it can be inferred as well
• It would be nice if we could automatically detect the equivalence between these two formulas
  • It would be nice if we could convert the implementation to the optimal solution
• It would be nice if we could generate an inverse of any formula (if possible)

  Probably requires a CAS

• It would be nice if we can compute the complexity of these functions
• It would be nice if we could compute the recurrence relation of these functions
• I'm not a math guru, how would we handle string operations?
• It would be nice if we could allow infinite sequences, test for convergence, return infinity if not
  • Optimize with convergence acceleration?
• Sequences are pretty parallel too

Related

• See mmlsharp project on Google Code, converts MathML to C#
• Sun's Project Fortress
  • Language follows math notation closely
  • Language is extremely extensible (for loop is a function; can be redefined)
• Fink
  • Follows math notation pretty well
  • Types expressed as constraints
  • Constraints are resolved at runtime
• wp:Constraint_programming, wp:Constraint_logic_programming