We will briefly list the components and features of the implemented framework. The full system documentation will be available from the Department of Artificial Intelligence at the University of Edinburgh. See chapter 7 for some examples of the capabilities of the most important components.
Two modules, “terms” and “oper_sem”, implement the abstract syntax and the operational semantics (evaluation rules) of our language as described in chapter 2.
The modules “types” and “typing” contain the type constructors and the typing rules. See chapter 2 for details again. Please note that we have extended the type system in other modules to allow polymorphic typing. This is not documented in our chapter on semantics — it is only an add-on. The additional polymorphic constructs and rules are contained in modules “poly_terms”, “poly_oper_sem”, “poly_types” and “poly_typing”. Background knowledge on polymorphic type inference can be found in []. It should also be noted that type checking is not fully working yet: unfortunately, time was too short to implement a complete algorithm that can handle recursive types in more than just trivial cases.
The monad we use for handling computational effects as described in chapter 6 is implemented in module “effect_monad”.
The partial evaluator as presented in chapter 6 can be found in module “part_eval”.
We make use of different kinds of “let”-terms so as to reflect the reason why some term has been lifted out of its place. All of them take a term as first argument and as second argument a function from terms to terms in which the first term should be substituted at runtime. This is implemented in module “let_ext”.
Besides a general “let” that does not make any assumptions
about its parameters, there is a “let_comp” and a
“let_mnont”. The latter two originate in the partial
evaluator: they replace the monad constructors of similar name
(“unit_comp_effM” and “unit_mnont_effM”). They indicate
whether some lifted expression is a terminating computation or maybe a
non-terminating one. This information can be used by other transformations
or program analysis predicates.
This functionality, which is implemented in module “termination”, allows the user to check whether evaluating a term will terminate (i.e. whether the term converges to a value). If this succeeds, the term is guaranteed to terminate, if it fails, it may still terminate but can also cause non-termination (generally undecidable). This component makes use of the information provided by the partial evaluator (the classification of computations into terminating and possibly non-terminating ones).
The module named “cse” (common sub-expression elimination), which also requires information provided by the partial evaluator, finds terminating computations that are duplicated in the program and replaces them with just one computation whose result is reused. Since it depends on results of the partial evaluator, its power also seems to depend on the capability to infer termination behaviour only: it should otherwise do a perfect job in the bounds of this limitation.
As described in section 6.3, there is an alternative implementation of the partial evaluator which maintains type annotations. This part comprises three modules: “tp_terms”, “tp_part_eval” and “tp_let_ext”. This partial evaluator reuses the monad to handle effects. It can also handle polymorphically typed programs, though there are still some unresolved issues concerning simplification of terms that require let-polymorphism. The current implementation takes a safe approach and does not simplify them. The corresponding rules are marked in the source code with a comment that contains “TODO”.
The implementation contains a utility module “utils” with commonly useful functionality, for example to eliminate subterms in LambdaProlog terms of arbitrary type. The current distribution also contains a generic Makefile that builds LambdaProlog projects and a VIM-syntax file for highlighting LambdaProlog source codes in the VIM-editor (Vi-Improved). Additionally, there is a small script “make_terzo.ml” written in OCaml plus an auxiliary LambdaProlog-module “terzo_stuff” which can be used to translate LambdaProlog sources that were written for use with Teyjus to source codes that can be accepted by the Terzo-implementation of LambdaProlog. The latter was very useful when it was not sure whether Teyjus, which was still under heavy development at the time of the project, had bugs or whether the program was incorrect. Comparisons with Terzo helped track down many bugs in the Teyjus-implementation1.