FASILL documentation Source fasill_unfolding

# Unfolding

This library provides predicates for unfolding FASILL programs.

Unfolding is a well-known, widely used, semantics-preserving program transformation operation which is able to improve programs, generating more efficient code. The unfolding transformation traditionally considered in pure logic programming consists in the replacement of a program clause $C$ by the set of clauses obtained after applying a computation step in all its possible forms on the body of $C$.

Let $\mathcal{P} = \langle\Pi,\mathcal{R},L\rangle$ be a FASILL program and let $R: A\leftarrow \mathcal{B} \in \Pi$ be a program rule with no empty body. Then, the classic unfolding of rule $R$ in program $\mathcal{P}$ is the new program $\mathcal{P}'= \langle\Pi', \mathcal{R}, L\rangle, \Pi' = (\Pi - \{R\}) \cup \{A\sigma\leftarrow \mathcal{B}' ~|~ \langle\mathcal{B};id\rangle \leadsto\ \langle\mathcal{B}';\sigma\rangle\}$.

In logic programming, classic unfolding preserves the computed answers and it leads to shorter derivations. However, in FASILL the classic unfolding may lose fca's when failure steps are involved, for some goals subsumed by the head of the unfolded rule. Furthermore, it may lead to wrong fca's when similarities are involved.

#### classic_unfold_by_id/1

classic_unfold_by_id( ?Id )

This predicate succeeds unfolding the FASILL rule Rule with identifier Id. This predicate has the side effect of retracting the rule Rule and asserting the new unfolded rules.

#### classic_unfold_by_id/2

classic_unfold_by_id( ?Id, ?Unfolded )

This predicate succeeds when Id is the identifier of a FASILL rule Rule and Unfolded is an unfolded rule of Rule.

#### classic_unfold/1

classic_unfold( +Rule )

This predicate succeeds unfolding the FASILL rule Rule. This predicate has the side effect of retracting the rule Rule and asserting the new unfolded rules.

#### classic_unfold/2

classic_unfold( +Rule, ?Unfolded )

This predicate succeeds when +Rule is a FASILL rule and Unfolded is an unfolded rule of Rule.

#### guards_unfold_by_id/1

guards_unfold_by_id( ?Id )

This predicate succeeds unfolding the FASILL rule Rule with identifier Id. This predicate has the side effect of retracting the rule Rule and asserting the new unfolded rules.

#### guards_unfold_by_id/2

guards_unfold_by_id( ?Id, ?Unfolded )

This predicate succeeds when Id is the identifier of a FASILL rule Rule and Unfolded is an unfolded rule of Rule.

#### guards_unfold/1

guards_unfold( +Rule )

This predicate succeeds unfolding the FASILL rule Rule. This predicate has the side effect of retracting the rule Rule and asserting the new unfolded rules.

#### guards_unfold/2

guards_unfold( +Rule, ?Unfolded )

This predicate succeeds when Rule is a FASILL rule and Unfolded is an unfolded rule of Rule.

#### is_safe_unfolding/2

is_safe_unfolding( +RegularGuards, +FailureBody )

This predicate succeeds when it is safe to perform a classic unfolding. I.e.: (∀ i ∈ {1,...,n}, \sigma_i is bound) ∧ [(∃ i ∈ {1,...,n}: \sigma_i = id) ∨ (B_{n+1} ≡ ⊥)].

#### vector_guards/2

vector_guards( +Vector, -Guards )
vector_guards( -Vector, +Guards )

Transform a list of guards Vector into a valid body Guards for the guards on control construct.

#### make_guard/3

make_guard( +Binds, -G1, -G2 )

This predicates makes the pair of guards G1-G2 from a list of bindings Binds.

#### bound_substitution/2

bound_substitution( +Substitution, ?BoundSubstitution )

This predicate succeeds when BoundSubstitution is Substitution restringed to its variables whose images are bound terms.

#### is_bound/1

is_bound( +Term )

Check if a term is bound.

#### unfold_by_id/1

unfold_by_id( ?Id )

This predicate succeeds unfolding the FASILL rule Rule with identifier Id. This predicate has the side effect of retracting the rule Rule and asserting the new unfolded rules.

#### unfold_by_id/2

unfold_by_id( ?Id, ?Unfolded )

This predicate succeeds when Id is the identifier of a FASILL rule Rule and Unfolded is an unfolded rule of Rule.

#### unfold/1

unfold( +Rule )

This predicate succeeds unfolding the FASILL rule Rule. This predicate has the side effect of retracting the rule Rule and asserting the new unfolded rules.

#### unfold/2

unfold( +Rule, ?Unfolded )

This predicate succeeds when Rule is a FASILL rule and Unfolded is an unfolded rule of Rule.