Cyclic Terms

In this file, we define when a PreGroundTerm is cyclic. This is exactly the case, when a function symbol contains twice in a nested fashion. For example $h(d, f(g(f(c))))$ is cyclic but $h(f(d), f(c))$ is not. Cyclic terms are mainly used to define MFA later.

The main result in this file then is cyclic_of_depth_too_big. That is, if a term exceeds a certain depth, then it is necessarily cyclic. This of course requires that only finitely many different function symbols are usable.

@[irreducible]

def PreGroundTerm.function_paths {sig : Signature} [DecidableEq sig.V] : FiniteTree (SkolemFS sig) sig.C → List (List (SkolemFS sig))

The function_paths of a PreGroundTerm are essentially all the (maximal) branches in the underlying finite tree without the terminal constant symbol. These can be used to detect cyclic terms by simply looking for repetitions along a branch.

Equations

• PreGroundTerm.function_paths (FiniteTree.leaf a) = [[]]
• PreGroundTerm.function_paths (FiniteTree.inner f ts) = if ts = [] then [[f]] else List.map (fun (path : List (SkolemFS sig)) => f :: path) (List.flatMap PreGroundTerm.function_paths ts)

@[irreducible]

def PreGroundTerm.contains_func {sig : Signature} [DecidableEq sig.V] (func : SkolemFS sig) : FiniteTree (SkolemFS sig) sig.C → Bool

A PreGroundTerm contains a function symbol if this symbols occurs as one of the inner labels.

Equations

• One or more equations did not get rendered due to their size.
• PreGroundTerm.contains_func func (FiniteTree.leaf a) = false

@[irreducible]

def PreGroundTerm.cyclic {sig : Signature} [DecidableEq sig.V] : FiniteTree (SkolemFS sig) sig.C → Bool

A PreGroundTerm is cyclic if one of its children contains_func the function symbol of the term or if one of its children is already cyclic. Constants are never cyclic.

Equations

• One or more equations did not get rendered due to their size.
• PreGroundTerm.cyclic (FiniteTree.leaf a) = false

theorem PreGroundTerm.function_path_elements_are_inner_labels {sig : Signature} [DecidableEq sig.V] (t : FiniteTree (SkolemFS sig) sig.C) (path : List (SkolemFS sig)) : path ∈ function_paths t → ∀ (f : SkolemFS sig), f ∈ path → f ∈ t.innerLabels

All elements of the function_paths paths are inner labels of the finite tree.

theorem PreGroundTerm.function_path_of_depth_exists {sig : Signature} [DecidableEq sig.V] (t : FiniteTree (SkolemFS sig) sig.C) : ∃ (path : List (SkolemFS sig)), path ∈ function_paths t ∧ path.length = t.depth - 1

There is a path in function_paths that matches the depth of the term (-1). That means that this path is one of maximal possible length.

theorem PreGroundTerm.function_path_elements_are_in_contains_func {sig : Signature} [DecidableEq sig.V] (t : FiniteTree (SkolemFS sig) sig.C) (path : List (SkolemFS sig)) : path ∈ function_paths t → ∀ (f : SkolemFS sig), f ∈ path → contains_func f t = true

For each element in a path from function_paths, contains_func is true.

theorem PreGroundTerm.cyclic_of_path_with_dup {sig : Signature} [DecidableEq sig.V] (t : FiniteTree (SkolemFS sig) sig.C) (path : List (SkolemFS sig)) (path_mem : path ∈ function_paths t) (dup : ¬path.Nodup) : cyclic t = true

A term is cyclic if a path in function_paths has a duplicate.

theorem PreGroundTerm.cyclic_of_depth_too_big {sig : Signature} [DecidableEq sig.V] [DecidableEq sig.C] (t : PreGroundTerm sig) (funcs : List (SkolemFS sig)) (nodup : funcs.Nodup) (funcs_in_t_from_funcs : ∀ (func : SkolemFS sig), func ∈ FiniteTree.innerLabels t → func ∈ funcs) : funcs.length + 2 ≤ FiniteTree.depth t → cyclic t = true

Consider a (deduplicated) list of possible function symbols and a term. If the depth of the term is at least the number of function symbols + 2, then the term must be cyclic.