General
Natural Semantics is based on Plotkin's Structural Operational Semantics (SOS) and further developed at INRIA by Kahn.
Specifications consist of data type declarations (abstract syntax, environments, run-time values, types, etc.) and sets of inference rules.
The inference rules specify relations between objects, in a style akin to Gentzen s Sequent Calculus for Natural Deduction. (Hence the name Natural Semantics.)
Achievements
- The Relational Meta-Language (RML) has been defined. It is strongly typed with a type system very much like that in Standard ML, has type-safe separate compilation and modules, and supports Natural Semantics-style inference rules. It has fewer non-declarative constructs than Prolog. The SML-like data types directly support structural-induction style specifications, which are central to Natural Semantics.
- The operational properties of RML were investigated and used to derive the initial implementation. A key component is the use of a Continuation-Passing Style (CPS) intermediate representation. CPS is easy to optimize, due to its declarative nature, but is also easily translated to low-level code, due to its simple operational semantics.
- Further observations lead to a refinement, whereby RML specifications are first translated to a First-Order Logic. High-level equivalences are used to rewrite this representation in order to reduce the amount of unnecessary non-determinism. This phase has proven to be essential for the practicality of the generated code.
- A compiler generating portable ANSI-C code has been implemented. The code runs unchanged on several different 32 and 64-bit architectures. Performance measurements indicate that this code runs several times faster than that generated by commercial Prolog compilers, and several orders of magnitude faster than TYPOL.
- Debugging facilities were added to the Relational Meta-Language (RML) system during 2002-2005 period.
|
|
