Format for Higher-Order Category

[AkihisaYamada]

I'd also like to propose two formats for higher-order rewriting, extending ARI's many-sorted TRS (MSTRS) format.

Although the HRS format allows arbitrary higher-order, the termCOMP category should be restricted to 2nd-order, since

• SOL adopts HRS semantics (for which confluence techniques exist), while
• Wanda chooses another semantics but it can support 2nd-order HRSs after translation.

Simply Typed TRS

Grammar

STTRS ::= (format STTRS) sort+ fun+ rule+
sort ::= (sort identifier )
fun ::= (fun identifier type )
type ::= identifier | (-> type+ identifier )
term ::= identifier | ( identifier term+ )

Syntactic restrictions

In each rule-decl:

1. The left- and right-hand sides must have the same type.
2. Variables in the right-hand side must occur in the left-hand side.
3. The left hand side must be a (lambda-free) pattern, i.e., no applied variables occur.

Semantics (Applicative)

1. Types and terms are applicative:

• (-> σ τ υ...) = σ → (-> τ υ...)
• (-> σ τ) = σ → τ
• ( s t... u ) = ( s t... ) u
• ( s t ) = s t

2. $→_R$ is the least rewrite relation containing $R$.

Examples:

Addition via id

(format STTRS)
; Except for the last line is a valid MSTRS.
(sort N)
(fun 0 N)
(fun s (-> N N))
(fun id (-> N N))
(fun + (-> N N N))
(rule (id x) x)
(rule (+ (s x) y) (s (+ x y)))
(rule (+ 0) id); not allowed in MSTRS

The map function

(format STTRS)
(sort N)
(sort L)
(fun nil L)
(fun cons (-> N L L))
(fun map (-> (-> N N) L L)); not allowed in MSTRS
(rule (map f nil) nil)
(rule (map f (cons x xs))
      (cons (f x) (map f xs)))

Map refinement

(rule (map id xs) xs)

Simply-Typed Lambda-Term Rewrite Systems

Grammar

The STLTRS grammar extends the STTRS grammar.

STLTRS ::= (format STLTRS) sort+ fun+ hrule+
hrule ::= (rule hterm aterm )
aterm ::= identifier | ( identifier hterm+ )
hterm ::= aterm | (lambda ( var+ ) hterm )
var ::= ( identifier type )

Syntactic Restrictions

In every rule:

1. The lhs and rhs must have the same type.
2. The free variables of rhs must occur free in the lhs.
3. The lhs must be a pattern, i.e., the arguments of every applied free variable are distinct bound variables.

HRS Semantics:

1. (rule l r ) represents the HRS rule $l^η → r^η$, where $⋅^η$ denotes the η-long form.
2. (rule (f p...) r) of function type represents $(f\ p...\ x...)^η → (r\ x...)^η$, where x... are fresh variables.
3. Note that (rule (f p...) (lambda (x...) r)) is not allowed. Write (rule (f p... x...) r) instead.

Examples

(format HRS)
; Except for the last line is a valid STTRS.
(sort N)
(sort L)
(fun nil L)
(fun cons (-> N L L))
(fun map (-> (-> N N) L L))
(rule (map f nil) nil)
(rule (map f (cons x xs))
      (cons (f x) (map f xs)))
(rule (map (lambda ((x N)) x) xs) xs)

; From Cynthia's note
(format HRS)
(sort R)
(fun + (-> R R R))
(fun deriv (-> (-> R R) R R))
(rule (deriv (lambda ((x R))
                     (+ (F x) (G x)))
             X)
      (+ (deriv F X) (deriv G X)))

[AkihisaYamada]

I fixed the description on Wanda.

[hezzel]

The existing higher-order category (which is incorrectly called "HRS") does plain matching union beta. If the argument for moving to HRSs is that it's the only format that is supported by more than one tool, that doesn't seem to apply in the termination case since more than one tool has participated in the termination competition in the past!

[AkihisaYamada]

I think it's reasonable to keep the plain matching union beta category, though it will remain as a demonstration. In this case,

1. Should it share the format with HRS?
   1. In this case, are you fine with (format HRS)?
   2. Otherwise, what name doesn't imply semantics?
2. Should it have another format? (I hope not, in this case, we'll introduce duplicates.)

[hezzel]

This question assumes that the inclusion of an HRS format is already decided, and I disagree that this should be the case. What is the argument for having an HRS category in the first place? And is that really a format that many people want?

It could well be -- I do not know what exactly everyone uses. However, I believe that this should be an integral part of the discussion, not the starting point. Note that the discussions so far have been (a) focused on the confluence competition, and (b) not held between people in higher-order rewriting.

My thoughts on this matter:

• My motivation for analysing higher-order rewriting focuses on program analysis, where modulo matching is not relevant, so I do not really have results on this (other than the inclusion of some fragments in the format I do use), nor am I likely to gain them in the future. My student, who is working on certifying termination techniques, is adamantly unwilling to support modulo matching (or even meta-variables). Hence, I would really prefer for the competition not to go in this direction. Although yes, that is a personal preference, and if the majority of people in higher-order rewriting truly wants HRSs I suppose I will cede this point -- but I would like to be sure that this is actually the case first, and not the result of a miscommunication.
• For 2nd-order HRSs, termination is equivalent to the corresponding 2nd-order CRS. However, making the format arbitrary-order but restricting what is actually used suggests the obvious direction for extension is arbitrary-type HRSs, rather than arbitrary-type CRSs, which might be preferable. Even if we end up with this second-order format, the formulation of the semantics is critical for the future.
• It is very possible that I have missed some papers due to my own focus, but at least for what I have seen, the vast majority of the termination results on term rewriting in the past 25 years were either on plain HO rewriting, or otherwise on rewriting with meta-variables, rather than full rewriting modulo beta and eta. It has also been the format in the termination competition for well over a decade, so existing implementations will typically at least support plain rewriting. So, there is no reason why plain rewriting union beta would be a demonstration category and HRS rewriting would not be.

I believe we could benefit from a discussion on exactly what formalism everyone is using and would prefer for the competition to support. For reference, see below for a simplified version of the formalism used by Wanda. (It is formulated as a proposal, since I previously wrote up this document as a suggestion for a possible extension of the existing "higher-order union beta" format. )

cms-simplified.pdf

[AkihisaYamada]

For TPDB, the motivation for the proposal is to define an ARI-friendly grammar for which the existing higher-order XMLs should be translated. I regret stepping into semantics.

I renamed the format to "simply-typed lambda-term rewrite systems" to avoid any indication of semantics. Do you think the grammar is OK?

Now for termCOMP. Note that there will be a category if a participant proposes it and SC agrees. I thought that a 2nd-order HRS category should be proposed, but now I'll stop this and see if a (the) participant will do this.

there is no reason why plain rewriting union beta would be a demonstration category and HRS rewriting would not be.

A category is called a competition if more than one participant participate, and a demonstration otherwise.

[AkihisaYamada]

How about adding an option to declare where lambda can occur? Some options are disallowed in (hypothetical) categories. Also it can be merged into STTRS format.

STTRS ::= (format STTRS (:lambda lambda-option)? )
lambda-option ::= R | LR

Adding more options like RROOT | LRROOT in future will be easy (I don't know they are useful).

Why do STTRSs not have a grammar rule for "rule"? (Is that because this is already in the mstrs syntax?)

Yes. The rules for "rule" and "term" are the same as (MS)TRS.

In the STLTRS grammar, I think "hrule ::= (rule hterm aterm )" should be "hrule ::= (rule aterm aterm )" or "hrule := (rule aterm hterm)" since I can't see why you would want to allow the left-hand side of a rule to be an abstraction.

Ah right, aterm aterm looks correct.

What's the benefit of the double brackets in the var of the lambda? Is there a risk of ambiguity by not having that?

It's imitation of SMT-LIB (and LISP, where (x) and x are different thing). The same "lambda" is proposed in SMT-LIB 3.0.

for "plain HO union beta" you would probably want to restrict left-hand sides to lambda-free patterns like in STTRSs, and may also want to forbid abstractions in left-hand sides altogether

I thought so too. (Though in the end retracted "right-lambda" variant.)

for "HRSs" you would probably want to require rules being in eta-long beta-normal form to avoid ambiguity (which excludes the map example as given, since for instance the first map rule would become: (rule (map (lambda ((x N)( (f x)) nil) nil)

Eta-normalized representation is to keep (make) TPDB compact. I've confirmed Makoto is fine with it.

[hezzel]

How about adding an option to declare where lambda can occur? Some options are disallowed in (hypothetical) categories. Also it can be merged into STTRS format.

What would be the point of that? It seems mostly relevant to people writing benchmarks, not to people writing parsers.

Eta-normalized representation is to keep (make) TPDB compact.

If you look at the benchmarks in the higher-order database, you'll see that even the large ones typically only have a small higher-order fragment. So this may just be premature optimisation.

I've confirmed Makoto is fine with it.

But I'm not. :)

At least ,it depends on the exact semantics -- again. "Eta-normalised representation" essentially forces a semantics modulo eta, since terms must be eta-expanded before being rewritten. If rules are presented in eta-long beta-normal form and all rules have base type, the semantics for second-order systems can be specified in a much simpler way -- and you do not get the same system having a completely different meaning in STTRS or HRS formats.

Note: I would be happy to write up a proposal for syntax and semantics (even for a second-order HRS format provided the category for plain HO union beta remains) in discussion with the others in the field, but it will have to wait until after the IJCAR deadline.

[AkihisaYamada]

What would be the point of that?

The point is to ease TPDB management and termCOMP organization. They have precedence over tool authors' convenience.

So this may just be premature optimisation.

Nooo, it is to avoid eta-equivalent variants in the DB.

But I'm not. :)

By "eta-nomalized" I intended lhs.

[AkihisaYamada]

Or do you mean none in the current database can be read as a pure STTRS in any sense? Then we cannot even have the STTRS category and defining the format is meaningless...

[hezzel]

Nooo, it is to avoid eta-equivalent variants in the DB.

If that's the goal, there is no reason to avoid eta-long beta-normal form (with base-type rules).

(In fact, it avoids the potential equivalent variants of f a -> b and f a x -> b x.)

By "eta-nomalized" I intended lhs.

Even so. This is more than just a syntactic choice: presenting rules in eta-normalised form even though an eta-expansion is sometimes needed to be able to apply a rule is a semantic choice, as it imposes reasoning modulo eta -- a choice that can be avoided altogether by presenting rules in eta-long form, as this ensures eta-longness is preserved under reduction. The semantics is much easier to specify in the expanded form.

Or do you mean none in the current database can be read as a pure STTRS in any sense?

No, that's not what I meant. There are plenty of applicative systems in the database, and most of the rest can be converted to it (although note that the termination behaviour could change because many terms are excluded in the STTRS setting).

What I meant is that if you require HRS rules to be presented in eta-long form, there is no possibility of confusion, because the only systems that are syntactically the same when written as an STTRS and written as an HRS are first-order systems.

[AkihisaYamada]

there will be a category if a participant proposes it and SC agrees

Actually this was not true.

[hezzel]

My counterproposal would be roughly the following:

• create one format, syntax and semantics, for higher-order rewriting, that covers STTRSs, plain higher-order rewriting with beta, and 2nd-order HRSs (this is doable with a syntax very much like what you already presented, and a semantics close to the one I linked in an attachment)
• the different styles then have different constraints on term formation:
  • in the STTRS category, interest is limited to terms constructed without lambda (and there is of course the requirement that rules do not use lambda -- and therefore automatically higher-order variables occur unapplied)
  • in the HRS category, interest is limited to terms of beta-normal eta-long form, and rules are required to be of base-type and in eta-long beta-normal form (note that for termination, the restriction on term formation actually has no effect so long as the restriction on rules is satisfied, but I do not know if the same applies to confluence)
  • in the HOUB category, there is no restriction on term formation (but we may or may not wish to limit interest to rules where variables in the left-hand side occur unapplied, as that largely matches with the semantics we currently have)

The downside of this proposal is that it will prevent reusability of benchmarks between the HRS category and the other two, since:

1. the format does allow "essentially the same" benchmark to be presented in multiple way -- e.g., (rule (map F (cons H T)) (cons (F H) (map F T)) and (rule (map (lambda ((x N)) (F x)) (cons H T)) (cons (F H) (map (lambda ((x N)) (F x)) T)
2. we cannot require that rules are presented in eta-long form due to the STTRS category, and we cannot require that they are presented in eta-short form due to the HRS category
3. most importantly, even without looking at categories we cannot require that rules are presented in either form because semantically these systems are not the same (and may have different termination / confluence behaviour, although this rarely happens)
4. and as an unfortunate consequence, not a single STTRS/HOUB benchmark could be used for HRS, and vice versa

I am not sure that this is avoidable, due to the real situation that semantically, eta-expanding a system changes its meaning -- at least for termination, but likely for confluence as well.

There is a possibility to still allow for some reuse, though:

• In the HRS category, instead of a limitation to the terms under consideration, a strategy is applied: after every reduction step, terms must be immediately beta-normalised and eta-expanded.
• Doing this, the following requirements on the rules would suffice (instead of being eta-long)
  • both sides have base type
  • the left-hand side is fully eta-expanded, except that variables are allowed to be unapplied
  • the right-hand side is not required to be eta-expanded

In this case, a rule (rule (map F (cons H T)) (cons (F H) (map F T)) would be usable in the HRS category, since the left-hand side of this rule does in fact match an eta-long term. However, a rule (rule (f sin X) -> X) would not be allowed if sin :: o -> o, because it would not be able to reduce an eta-long term -- as this would have the form (f (lambda ((z o)) (sin s)).

In addition, to limit duplicates, we could use the guideline that variables should be presented in eta-short form if doing so would not change the meaning / typical behaviour of the TRS. (Though this is a rather wishy-washy guideline -- and I cannot be more concrete without studying confluence first ,as I do not yet know the situaitons in which this choice would matter.)

[hezzel]

This shared format would have the following syntax:

hotrs ::= (FORMAT STTRS|CFS|CMS|HRS) sort+ fun+ hrule+
sort ::= (SORT IDENTIFIER )
fun ::= (FUN IDENTIFIER type )
type ::= IDENTIFIER | (-> type+ IDENTIFIER )
term ::= IDENTIFIER | ( IDENTIFIER term+ ) | (LAMBDA (var+) term)
var ::= ( IDENTIFIER type )
rule ::= (RULE term term)

And the following restrictions that are always in place:

1. The left- and right-hand sides must have the same type.
2. Variables in the right-hand side must occur in the left-hand side.
3. The left-hand side has the form (f l1 ... ln) with f a function symbol.
4. The left-hand side must be a pattern, i.e., the arguments of every applied free variable are distinct bound variables.
5. If any variable occurs applied on the left, then each occurrence (both in left- and right-hand side) must have exactly the same number of arguments. (But if a variable only occurs unapplied on the left, it is allowed to occur applied on the right.)

They would also share the following notion of reduction:

• A _meta-substitution _ subst for a rule l -> r is a function that maps:
  • each variable F that occurs unapplied in l to a term of the same type
  • each variable F that occurs with n arguments in l to an expression [x1...xn] t, where lambda x1...xn.t is a term of the same type as F
• Applying a meta-substitution combines the usual (plain) notion of substitution with a beta-development:
  • (f s1 ... sn) subst = f (s1 subst) ... (sn subst)
  • (x s1 ... sn) subst = subst(x) (s1 subst) ... (sn subst) if subst(x) is a term (so x occurs unapplied in l)
  • (x s1 ... sn) subst = t[y1:=s1 subst,...,yn:=sn subst] if subst(x) = [y1 ... yn] t
  • (lambda x1...xn.s) subst = lambda x1...xn.(s subst) if x1,...,xn do not occur in either domain or range of subst
• Note that, by restriction 5, if subst is a meta-substitution for l -> r, then both l subst and r subst are well-defined terms
• We say s -> t if s = C[l subst] and t = C[r subst] for l -> r a rule, subst a meta-substitution for this rule, and C a context
• We also let s -> t if s beta-reduces to t in a single step.

(Essentially, applied variables are used as syntactic sugar for meta-application.)

Then different formats operate under different restrictions and strategies:

CMS (curried meta-variable systems)

This formalism is entirely unrestrained: all well-typed terms that can be constructed are allowed, all rules that can be constructed are allowed.

CFS (curried functional system -- aka plain higher-order rewriting union beta)

Term formation is unrestricted, but arestriction is imposed on the rules: all variables must occur unapplied in the left-hand sides of a rule. Hence, meta-substitution just becomes substitution.

STTRS (simply-typed term rewriting system)

Term formation is restricted: we only consider terms that are constructed without using abstraction.

This also imposes the following syntactic restrictions on the rules:

• no lambda occurs in either side of a rule
• hence, in left-hand sides all variables must occur unapplied

HRS option 1 (higher-order rewriting systems with pattern restrictions)

Term formation is restricted: we only consider terms in beta-normal eta-long form.

This imposes the following requirements on rule formation:

• All rules have base type.
• All rules are presented in eta-long beta-normal form.

In a second-order HRS, the semantics given above rewrites eta-long beta-normal terms to beta-normal eta-long terms, so this definition is unproblematic. However, in third-order HRSs and above, this is not necessarily the case. Hence, we must adapt the notion of reduction: s -> t if s = C[l subst] and t = C[r subst]\downarrow_beta.

HRS option 2 (higher-order rewriting systems with pattern restrictions, alternative formulation)

To accommodate reuse of benchmarks, we can also use the following equivalent definition for HRSs: term formation is not restricted, but reduction is:

• We use a reduction strategy that prioritises beta-normalisation, followed by eta-expansion, and only then reduction using rules.
• Hence, only terms in eta-long beta-normal form may be reduced by a rule.

For this to make sense, we impose the following additional requirements on rule formation:

• Left-hand sides of rules are in semi-eta-long form.
• Both left- and right-hand sides of rules are in beta-normal form.

Here, semi-eta-long form is defined as follows:

• f s1 ... sn is in semi-eta-long form if it has base type, and each si is in semi-eta-long form
• x s1 ... xn is in semi-eta-long form if it has base type, and each si is in semi-eta-long form
• lambda x.s is in semi-eta-long form if s is
• every variable is in semi-eta-long form

(Rules that do not satisfy these requirements cannot be applicable on eta-long terms.)

What do you think?

(A disclaimer: I strongly believe that this semantics is equivalent to standard HRS semantics, but I have not formally proved it -- though it seems straightforward with existing translation results.)

[AkihisaYamada]

(Though I do not fully understand your proposal)

• From the TPDB point of view, "variables have to be eta-short" should be good.
• I understand eta (on function symbols) can make difference depending on semantics (it is the case in Isabelle/HOL's higher order rewriting).
• Differentiating format by semantics is not intended. (Semantics is up to competition categories.)
• Mayr & Nipkow defines HRS as a set of rules [https://www.sciencedirect.com/science/article/pii/S0304397597001436]. So (format HRS) shouldn't be too bad.

[AkihisaYamada]

(I don't see what the purpose of the line...

I agree (from the termCOMP view. It was introduced with the CoCo-infra in mind).

Imposing "variables have to be eta-short" as a strict rule might be too strong, since there are cases where it would affect termination (for example, f (lambda x.Z[x]) -> f h is terminating if h is a constructor of higher type, but f Z -> f h is non-terminating).

Ah I see. I have nothing against having benchmarks which are equivalent in some categories but different in another.

[ffrohn]

• Differentiating format by semantics is not intended. (Semantics is up to competition categories.)

Why? I think format should indicate what kind of system is given. Then the competition categories specify which property should be analyzed (innermost termination, full runtime complexity, ...).

[ffrohn]

Would a guideline "variables should be eta-short but exceptions can be made if eta-shortening would affect termination or confluence" be reasonable for the way the TPDB and competitions are planned to operate in the future?

From the point of view of someone who knows little about higher order rewriting, that sounds like a guideline that's difficult to check / maintain. Someone who can judge whether "eta-shortening would affect termination or confluence" would have to check all submitted benchmarks manually, correct?

[hezzel]

I don't know how you intend to run the database and maintain these rules against duplication! So this could be impractical for what you had in mind. But what I meant was just that in principle people follow the guideline, and if they deviate they should justify why. (In practice I expect that this would stop accidental submissions of benchmarks that violate the guideline, but allow for the one or two expanded benchmarks that someone deliberately wants to put in.)

[ffrohn]

I don't know how you intend to run the database and maintain these rules against duplication!

I think whoever maintains the TPDB can only enforce rules / guidelines that can easily be checked automatically. So if we fix guidelines that cannot be checked automatically, then sooner or later, benchmarks that violate these guidelines will end up in the TPDB.

Still, having such guidelines might make sense, since they justify the removal of such benchmarks when they are discovered. So regarding your question

Would a guideline ... be reasonable for the way the TPDB and competitions are planned to operate in the future?

from my point of view, the answer is yes, as long as we all agree that the maintainer(s) of the TPDB are not to blame if benchmarks that violate the guideline slip through.

[AkihisaYamada]

• Differentiating format by semantics is not intended. (Semantics is up to competition categories.)

Why? I think format should indicate what kind of system is given. Then the competition categories specify which property should be analyzed (innermost termination, full runtime complexity, ...).

The thing complicating the thread is still which property of the same set of rules should be analyzed: termination modulo beta, beta-eta, union beta, beta-eta long, ...

I'd propose

• priority is on beta-eta short form, but
• allow beta-/eta-redexes with excuse as a comment
• If someone finds such an excuse invalid, then organizers can remove the benchmark

[ffrohn]

The thing complicating the thread is still which property of the same set of rules should be analyzed: termination modulo beta, beta-eta, union beta, beta-eta long, ...

Ok, but that's analogous to other categories. E.g., for complexity, we'll use the same format for full/innermost runtime/derivational complexity, and then the question whether full runtime complexity or innermost derivational complexity or ... is fixed by the category.

priority is on beta-eta short form, but
allow beta-/eta-redexes with excuse as a comment
If someone finds such an excuse invalid, then organizers can remove the benchmark

Sounds reasonable to me.

[hezzel]

We are still talking about eta-short variables aren't we?

Rules should not by default be eta-short. That would be horrible (especially since HRS semantics requires at least left-hand sides to be eta-long).

As for beta: if someone submits a rule where the left-hand side is not beta-normal, then that is clearly intentional and very much not semantically equivalent to its beta-normal form (as doing this creates a critical pair with the beta rule, which affects both termination and confluence). Such a rule also could not be used for HRS reduction.
In the right-hand side it would make sense to add the rule that it should be beta-normal unless justified otherwise. (But note: it is quite unlikely that someone would add a non-beta-normal rhs by accident..)

[AkihisaYamada]

Ok, but that's analogous to other categories.

Yes, I mean hence the (format line should not specify the information.

We are still talking about eta-short variables aren't we?

OK I guess so.

As for beta: if someone submits a rule where the left-hand side is not beta-normal, then that is clearly intentional

Allowing beta-reducible lhs would be significant enough to be a different category...

[hezzel]

Ah yes, we should probably just exclude non-beta-normal left-hand sides altogether (arguably, it's not a pattern).

[hezzel]

There is one potential purpose of the format line: to indicate what sorts of restrictions the example satisfies. For example, whether it is an STRS (so: no lambdas) or an HRS (so: eta-long left-hand side) or even both.

Is this useful information to keep track of? Alternatively, it could be a list of properties.

So you could for example have:

(format STRS CFS HRS CMS)

Or alternatively you could have

(properties Applicative Metafree Leftlong)

Or just no property/format line at all.

What would you prefer?

[ffrohn]

Aren't these restrictions similar to the tags that are used in ARI-COPS (ground, left-linear, right-ground, srs, ...)? I think it would be nice to have something like that in the future, but such tags shouldn't be part of the input file, in my opinion.

No format line at all would be inconsistent with the other categories. Can we use something non-controversial / something that does not have undesired semantic implications as format? How about (format higher-order)?

[hezzel]

I don't know about ARI-COPS (not being part of the ARI project), but maybe?

However, I am not sure if the motivation is similar. The reason to include something like this would be to know which benchmarks are suitable for which categories / competitions. It seems that the confluence competition is going to consider HRS input -- this means that they can only use "leftlong" benchmarks. And if we have an STRS category in the termination competition, this can only use lambdafree benchmarks. So whether these tags are needed kind of depends on how you were planning on running the competitions from this database in the future!

I will include the non-controversial (format higher-order) line in the generated benchmarks. :)

[AkihisaYamada]

I'm second to Florian's suggestion. COPS doesn't have a directory structure, so the format line make more sense than for TPDB.

We'll have no problem with the same format line in different folders.

[ffrohn]

The conversion is done (thanks @hezzel!), so I think we can close this discussion.