term

lpo

package lpo

Provides functionality needed for lexicographic path ordering (LPO).

Overview

An LPO needs a precedence on function symbols which is provided by class term.lpo.Precedence.

Visibility
  1. Public
  2. All

Type Members

  1. class Precedence extends AnyRef

    Represents a precedence on function symbols.

  2. type Rel = List[(F, F)]

    Represents a relation on function symbols.

    Represents a relation on function symbols.

    Definition Classes
    package

Value Members

  1. object PrecParser extends RegexParsers

    A parser to parse a precedence from a string.

  2. def lpo (trs: TRS, p: Precedence): (Boolean, Precedence)

    Returns the tuple (lpob,lpop).

    Returns the tuple (lpob,lpop).

    Definition Classes
    package

  3. def lpob (trs: TRS, p: Precedence): Boolean

    Returns true if the term rewrite system trs can be shown terminating using LPO and false otherwise.

    Returns true if the term rewrite system trs can be shown terminating using LPO and false otherwise.

    Definition Classes
    package

  4. def lpop (trs: TRS, p: Precedence): Precedence

    Returns the precedence on function symbols in trs which can show trs terminating with lpo.

    Returns the precedence on function symbols in trs which can show trs terminating with lpo.

    Definition Classes
    package