Higher Order Rewriting
- Allow lambda binders.
- Use Church simply type lambda calculus without type variables. No type constructors by now.
- Same type for both sides of the rule.
- Typability is guaranteed.
- Function declaration distinguishes between input (argument) types and the output type. The input and output types can be functional (include arrows). As an example
f: (int , int , (int -> int) ) -> (int->int)
has three input types (where the third one is functional) and a functional output. Thus if a:int then we can have
(f(a,a,\lam x.a) a)
as a term. Functions can only be used with all its arguments. For writing examples in applicative form, one can define f as:
f: () -> (int -> int -> (int -> int) -> int -> int)
then the term would be
(f a a \lam x.a a)
- Rewriting with matching modulo alpha and union beta.
- Rewriting with higher-order pattern matching on beta-normal eta-long forms (HRS). In this case, left and right hand sides are assumed to be normalized.
- Other categories may be considered in the near future. For instance, we can add STTRS and use the problem families without binders, but with a different semantics.
- We postpone certification for the future.
A precise syntax following the standards of the TPDB will be defined very soon.
Comments are welcome.