Module Export.HrsSource

This module provides a function to translate a signature to the HRS format used in the confluence competition.

• see http://project-coco.uibk.ac.at/problems/hrs.php

  .

• Lambdapi terms are translated to the following HRS term algebra with a unique type t:

A : t -> t -> t // for application

L : t -> (t -> t) -> t // for λ

B : t -> t -> (t -> t) -> t // for let

P : t -> (t -> t) -> t // for Π

Function symbols and variables are translated as symbols of type t.

Pattern variables of arity n are translated as variables of type t -> ... -> t with n times ->.

• In the hrs format, variable names must be distinct from function symbol names. So bound variables are translated into positive integers and pattern variables are prefixed by "$".

• There is no clash between function symbol names and A, B, L, P because function symbol names are fully qualified.

• Function symbol names are fully qualified but "." is replaced by "_" because "." cannot be used in identifiers ("." is used in lambda abstractions).

• Two occurrences of the same pattern variable name may have two different arities (in two different rules). So pattern variable names are prefixed by the rule number.

TO DO:

• HRS does not accept unicode characters.

• Optim: output only the symbols used in the rules.