comp_duals.pl -- Dual rule computation

Computation of dual rules (rules for the negation of a literal).

author: - Kyle Marple
version: - 20170127
license: - BSD-3

Compute rules for the negations of positive literals (dual rules), even if there are no clauses for the positive literal (negation will be a fact). Wrapper for comp_duals2/1.

comp_dual(+Predicate) is det[private]

get matching rules and call comp_duals3/2.

comp_duals3(+Predicate:atom, +Rules:list) is det

Compute the dual for a single positive literal. Make sure that Predicate is used for the dual head instead of taking the head from one of the rules. This allows a new head to be passed during NMR sub-check creation.

Arguments:

`Predicate`	- The head of each rule in `Rules`, of the form Head/arity.
`Rules`	- The list of rules for a single predicate.

comp_dual(+DualHead:compound, +Rules:list, -DualBody:list, +Count:int) is det[private]

Compute the dual for a predicate with multiple rules. First, compute the dual of each individual rule, replacing each head with a new, unique one. Then create the overall dual using the heads of the individual duals as goals. When finished, assert the overall dual.

Arguments:

`DualHead`	- The head of the dual rule.
`Rules`	- The list of rules.
`DualBody`	- The body of the outer dual rule.
`Count`	- Counter used to ensure that new heads are unique.

comp_dual2(+DualHead:compound, +Body:list, +BodyVars:list) is det[private]

Compute the dual for a single clause. Since any body variables in the original rule are existentially, they must be universally quantified in the dual. This is accomplished by creating a new predicate with both the original head variables and the body variables in the head, which will contain the duals of the original goals. The "inner dual" will then call this new predicate in a forall over the body variables.

Arguments:

`DualHead`	- The head of the dual rule.
`Body`	- The body of the original rule.
`BodyVars`	- The list of variables in the body but not the head.

comp_dual3(+DualHead:compound, +Body:list, +UsedGoals:list) is det[private]

Compute the innermost dual for a single rule by negating each goal in turn. Unlike grounded ASP, it is not enough to have a single-goal clause for each original goal. Because side effects are possible, the sub-dual for a given goal must include all previous goals and retain program order.

Arguments:

`DualHead`	- The head of the dual rule.
`Body`	- The body goals to negate.
`UsedGoals`	- The goals that have already been processed, in original order.

dual_goal(+GoalIn:compound, -GoalOut:compound) is det[private]

Given a goal, negated it.

Arguments:

`GoalIn`	- The original goal.
`GoalOut`	- The negated goal.

define_forall(+GoalIn:compound, -GoalOut:compound, +BodyVars:list) is det

If BodyVars is empty, just return the original goal. Otherwise, define a forall for the goal. For multiple body variables, the forall will be nested, with each layer containing a single variable.

Arguments:

`GoalIn`	- Input goal.
`GoalOut`	- Output goal.
`BodyVars`	- Body variables present in `GoalIn`.

outer_dual_head(+Head:atom, -DualHead:compound) is det[private]

Create the dual version of a rule head by negating the predicate name and replacing the args with a variable list of the same arity.

Arguments:

`Head`	- The initial, positive head, a predicate name.
`DualHead`	- The dual head, a predicate struct.

abstract_structures(+ArgsIn:list, -ArgsOut:list, +Counter:int, -Goals:list) is det[private]

Given a list of args, abstract any structures by replacing them with variables and adding a goal unifying the variable with the structure.

Arguments:

`ArgsIn`	- The original args from a clause head.
`ArgsOut`	- Output new args.
`Counter`	- Input counter.
`Goals`	- `Goals` unifying non-variables with the variables replacing them.

prep_args(+OrigArgs:list, +VarArgs:list, +NewArgsIn:list, -NewArgsOut:list, +VarsSeen:list, +Counter:int, -Goals:list) is det[private]

Given two sets of args, check if each of the original args is a variable. If so, check if it's a member of NewArgsIn. If it's not, add it to output args. If it isn't a variable, or the variable is present in NewArgsIn, add the corresponding variable from VarArgs. The result is a list of variables that keeps any variables in the original head. When an element from VarArgs is used, add a unification (=) goal to Goals.

Arguments:

`OrigArgs`	- The original args from a clause head.
`VarArgs`	- A list of unique variable names of the same length as `OrigArgs`.
`NewArgsIn`	- Input new args.
`NewArgsOut`	- Output new args.
`VarsSeen`	- List of variables encountered in original args.
`Counter`	- Input counter.
`Goals`	- `Goals` unifying non-variables with the variables replacing them.

prep_args2(+ArgsIn:list, -ArgsOut:list, +VarsSeenIn:list, -VarsSeenOut:list, +CounterIn:int, -CounterOut:int, -UniGoals:list) is det[private]

Given the arguments from a compound term, create unifiability goals to be used in the dual.

Arguments:

`ArgsIn`	- Input args.
`ArgsOut`	- Output args.
`VarsSeenIn`	- Input vars seen.
`VarsSeenOut`	- Output vars seen.
`CounterIn`	- Input counter.
`CounterOut`	- Output counter.
`UniGoals`	- List of unification goals.