back to the tutorial home page
back to the MGS home page
Topological collection can be seen as a generalization of the notion of containers developed in the standard C++ library or in JAVA. We are currently trying to developp several API to offer the idea of topological collection in these languages. One problem is the specification of transformation: without an ad hoc syntax, the definition of a rule is very painful.
The implementation of the functional evaluator of MGS relies on a higher-order abstract syntax approach (HOAS). THe HOAS form of a MGS term is obtained by a combinatorisation using a subset of the combinators introduced by Dillers. You will fnd the technical details in:
C
) and prove the correction of the approach using the Coq theorem prover. The resulting evaluation function is rather efficient: more efficient than Mathematica or Python a heavily recursive function (ackermann, fibonacci, factorial, etc.).