Evolog - Support for actions and program modularization

[madmike200590]

Support for actions and program modularization

• Adds support for action rules, i.e. rules that call procedures with side-effects (e.g. writing to a file) when firing.
• Adds support for modules, which enable using ASP-programs as subroutines which can be used in a main program similar to external atoms

Detailed formal semantics for both actions and modules are described in Chapter 3 of [1].

Action Rules

Overview

Action rules allow for so-called side-effects in an ASP program, i.e. when an action rule fires, certain changes (such as opening or writing to files) can be applied to the environment. Consider the following Hello World-style example:

hello_text("Hello World!").
hello_result(R) : @streamWrite[STDOUT, TEXT] = R :- hello_text(TEXT), &stdout(STDOUT).

The rule on line 2 is an action rule:

• hello_result(R) : @streamWrite[STDOUT, TEXT] = R is an action head, where hello_result(R) is a regular head atom, but @streamWrite[STDOUT, TEXT] = R references an action function that has 2 input terms (variables STDOUT and TEXT) and yields the result term R.
• When the body of an action rule is considered to be true (i.e. the rule fires), the action function is called.
• In the example, the action function @streamWrite[STDOUT, TEXT] writes the string TEXT to the file descriptor STDOUT. Variable STDOUT is bound by an external atom &stdout(STDOUT) which always supplies a reference to the standard output stream.

Semantics and Restrictions

To stay in line with ASPs declarative semantics, action rules in Alpha

• may only apply their action function to the "outside world" once, regardless of how often the solver internally evaluates the rule. Applied to the hello world example, an implementation needs to make sure Hello World! is only written to the console once, regardless of the solver's actual evaluation strategy.
• may only occur in programs that are fully stratifiable (in their nonground version, stratifying by predicates as implemented in PR Partial up-front evaluation of stratifiable program parts - issue #75 #207 ). This is to ensure that all action results are part of an answer set so that whenever a side-effect is applied, there is an atom in an answer set "witnessing", i.e. making transparent said side-effect.

Implementation

Rules with action heads are modelled as instances of NormalRule whose head is an instance of ActionHead:

public interface ActionHead extends NormalHead {
	String getActionName();
	List<Term> getActionInputTerms();
	VariableTerm getActionOutputTerm();
}

Interpretation of rules with action heads

Due to the restriction on program structure stated above, where actions may only occur in stratifiable programs, interpretation of action heads is implemented directly in StratifiedEvaluation.
Given a satisfying substitution for the body, fireRule checks whether the head of the rule in question is an ActionHead and, if so, calls instantiateActionHead:

public BasicAtom instantiateActionHead(ActionHead head, Substitution substitution, CompiledRule rule) {
	List<Term> actionInput = head.getActionInputTerms();
	List<Term> substitutedInput = new ArrayList<>();
	// Substitute all variables in action input so that all input terms are ground.
	for (Term inputTerm : actionInput) {
		substitutedInput.add(inputTerm.substitute(substitution));
	}
	// Delegate action execution to respective backend.
	ActionWitness witness = actionExecutionService.execute(head.getActionName(), rule.getRuleId(), substitution, substitutedInput);
	// If the according debug flag is set, convert witness to atom and add to facts.
	if (generateActionWitnesses) {
		BasicAtom witnessAtom = buildActionWitnessAtom(witness, rule);
		// Note that this is a rather "sneaky" side-effect,
		// but seems like overkill to do this structurally proper just for a debug feature.
		workingMemory.addInstance(witnessAtom, true);
	}
	// We have an action result. Add it to the substitution as the substitute for the variable bound to the action so we're able to obtain the
	// ground BasicAtom derived by the rule
	substitution.put(head.getActionOutputTerm(), witness.getActionResult());
	return head.getAtom().substitute(substitution);
}

Here, the actual action (i.e. the side-effect modifying the state of the outside world) is performed by calling an ActionExecutionService. The result of this call is an ActionWitness which represents the information from a head atom of an action application rule as described in section 3.1 of [1]. The atom that is added to an answer set as a result of firing a rule with an action head, is obtained from the ActionWitness:

	substitution.put(head.getActionOutputTerm(), witness.getActionResult());
	return head.getAtom().substitute(substitution);

This atom is exactly what is described as the head atom of an action projection rule in section 3.1 of [1].

It's important to note that a distinct action is only ever executed once, i.e. even if the exact same rule is grounded and fired more than once, the resulting side-effect is only applied once. This is achieved through caching of action results in ActionExecutionServiceImpl:

public class ActionExecutionServiceImpl implements ActionExecutionService {
        .....
	@Override
	public ActionWitness execute(String actionName, int sourceRuleId, Substitution sourceRuleInstance, List<Term> inputTerms) {
		ActionInput actInput = new ActionInput(actionName, sourceRuleId, sourceRuleInstance, inputTerms);
		return actionRecord.computeIfAbsent(actInput, this::execute);
	}
	....
}	

Program Modularization

The second major part of this PR is program modularization. It adds ModuleAtoms as possible form of a body atom. Conceptually, a ModuleAtom works like an external atom - based on some input terms, a (side-effect-free) function is evaluated and the function result is assigned to a list of output terms.
In the case of a module atom, the function in question is the evaulation of an ASP program, where the atom's input terms are translated to facts that get added to said program. Each answer set of the module program is transformed into a list of terms that make up the output terms for one ground instance of the module atom.
A module atom yields one ground instance per answer set for each unique combination of input terms. The detailed formal syntax and semantics of Modules are described in Section 3.2 of [1].

Module definitons and usage in rules

An ASP-program that can be used as a module atom in other programs needs to be defined within a #module ...-Section, e.g.:

%%% Module threecol %%%
%
% Calculates 3-colorings of a given graph.
% Graph is expected to be represented as a function term with following
% structure: graph(list(V, TAIL), list(E, TAIL)), where list(V, TAIL)
% and list(E, TAIL) are vertex- and edge-lists.
%
%%%
#module threecol(graph/2 => {col/2})  {
	% Unwrap input
	vertex_element(V, TAIL) :- graph(lst(V, TAIL), _).
	vertex_element(V, TAIL) :- vertex_element(_, lst(V, TAIL)).
	vertex(V) :- vertex_element(V, _).
	edge_element(E, TAIL) :- graph(_, lst(E, TAIL)).
	edge_element(E, TAIL) :- edge_element(_, lst(E, TAIL)).
	edge(V1, V2) :- edge_element(edge(V1, V2), _).

	% Make sure edges are symmetric
	edge(V2, V1) :- edge(V1, V2).

	% Guess colors
	red(V) :- vertex(V), not green(V), not blue(V).
	green(V) :- vertex(V), not red(V), not blue(V).
	blue(V) :- vertex(V), not red(V), not green(V).

	% Filter invalid guesses
	:- vertex(V1), vertex(V2), edge(V1, V2), red(V1), red(V2).
	:- vertex(V1), vertex(V2), edge(V1, V2), green(V1), green(V2).
	:- vertex(V1), vertex(V2), edge(V1, V2), blue(V1), blue(V2).

	col(V, red) :- red(V).
	col(V, blue) :- blue(V).
	col(V, green) :- green(V).
}

In the module declaration at the start of the section (i.e. #module threecol(graph/2 => {col/2})), threecol is the name (i.e. unique identifier) of the module, graph/2 is an input predicate, and {col/2} denotes the set of output predicates for the module. Note that there may be multiple input predicates as well as output predicates.

A program using the above module definition to calculate 3-colorings of a graph could look as follows:

vertex(a).
vertex(b).
vertex(c).
edge(a, b).
edge(b, c).
edge(c, a).

vertex_list(VLST) :- VLST = #list{V : vertex(V)}.
edge_list(ELST) :- ELST = #list{edge(V1, V2) : edge(V1, V2)}.

coloring(COL) :- vertex_list(VERTEX_LST), edge_list(EDGE_LST), #threecol{2}[VERTEX_LST, EDGE_LST](COL).

Looking at the module atom #threecol{2}[VERTEX_LST, EDGE_LST](COL),

• threecol denotes the name of the module
• {2} is the number of answer sets that should be calculated. This can be omitted, in which case all answer sets are calculated
• VERTEX_LST and EDGE_LST are input terms
• COL is an output term

The sole answer set of the program above is:

{ coloring(lst(col(a, red), lst(col(b, blue), lst(col(c, green), lst_empty)))), coloring(lst(col(a, red), lst(col(b, green), lst(col(c, blue), lst_empty)))), edge(a, b), edge(b, c), edge(c, a), edge_list(lst(edge(a, b), lst(edge(b, c), lst(edge(c, a), lst_empty)))), vertex(a), vertex(b), vertex(c), vertex_list(lst(a, lst(b, lst(c, lst_empty)))) }

Note that each graph coloring calculated by the threecol-module is represented as one coloring-Atom. The term holding the actual coloring is structured as a list-term (see below) and holds the assigned color for each vertex.

List Terms

Since module atoms can only accept and yield terms as inputs and outputs, list terms were intoduced as a means of grouping multiple terms into one.
A list term representing the list [a, b, c] is written lst(a, lst(b, lst(a, lst_empty))), i.e. a list term is a binary function term with function symbol lst whose first argument is the head element of a list, and the second argument is the remainder (i.e. tail) of the list. The constant lst_empty represents the empty list.

The aggregate function #list can be used to group instances of a predicate into a term list, as demonstrated in the rule to construct a vertex list: vertex_list(VLST) :- VLST = #list{V : vertex(V)}. In the example above, the resulting atom is vertex_list(lst(a, lst(b, lst(c, lst_empty)))).

If a program needs to pass in multiple terms into a module atom, this can be achieved suing list terms as demonstrated above. The module program then needs to unwrap the list term accordingly (see example above).

Since one ground instance of a module atom always corresponds to one answer set for a given substitution of input terms, atoms within that answer set are also represented as list terms, as can be seen in the above example, where one coloring is represented as coloring(lst(col(a, red), lst(col(b, green), lst(col(c, blue), lst_empty)))).

Interpretation of module atoms

In Alpha, module atoms are implemented as follows:
During parsing, module definitions (i.e. ASP subprograms constituting modules) are written into a list of modules that is attached to the main program:

	public Object visitDirective_module(ASPCore2Parser.Directive_moduleContext ctx) {
		if (!programBuilders.empty()) {
			throw new IllegalStateException("Module directives are not allowed in nested programs!");
		}
		// directive_module: SHARP DIRECTIVE_MODULE id PAREN_OPEN module_signature PAREN_CLOSE CURLY_OPEN statements CURLY_CLOSE;
		String name = visitId(ctx.id());
		ImmutablePair<Predicate, Set<Predicate>> moduleSignature = visitModule_signature(ctx.module_signature());
		startNestedProgram();
		visitStatements(ctx.statements());
		InputProgram moduleImplementation = endNestedProgram();
		currentLevelProgramBuilder.addModule(Modules.newModule(name, moduleSignature.getLeft(), moduleSignature.getRight(), moduleImplementation));
		return null;
	}

Module atoms are represented as a specific kind of atom after parsing and cannot be directly grounded (i.e. evaluated) like external atoms:

	@Override
	public ModuleAtom visitModule_atom(ASPCore2Parser.Module_atomContext ctx) {
		// module_atom : SHARP id (CURLY_OPEN NUMBER CURLY_CLOSE)? (SQUARE_OPEN input = terms SQUARE_CLOSE)? (PAREN_OPEN output = terms PAREN_CLOSE)?;
		String moduleName = visitId(ctx.id());
		ModuleAtom.ModuleInstantiationMode instantiationMode;
		if (ctx.NUMBER() != null) {
			instantiationMode = ModuleAtom.ModuleInstantiationMode.forNumAnswerSets(Integer.parseInt(ctx.NUMBER().getText()));
		} else {
			instantiationMode = ModuleAtom.ModuleInstantiationMode.ALL;
		}
		List<Term> inputTerms = visitTerms(ctx.input);
		List<Term> outputTerms = visitTerms(ctx.output);
		return Atoms.newModuleAtom(moduleName, instantiationMode, inputTerms, outputTerms);
	}

The actual linking from module atoms to the corresponding module definitions happens in a ProgramTransformation called ModuleLinker. Here, for each module atom, an actual ExternalAtom is constructed, which runs the program from the module definition:

public class ModuleLinker extends ProgramTransformation<NormalProgram, NormalProgram> {

	// Note: References to a standard library of modules that are always available for linking should be member variables of a linker.
	private final Alpha moduleRunner;

	public ModuleLinker(Alpha moduleRunner) {
		this.moduleRunner = moduleRunner;
	}


	@Override
	public NormalProgram apply(NormalProgram inputProgram) {
		Map<String, Module> moduleTable = inputProgram.getModules().stream().collect(Collectors.toMap(Module::getName, Function.identity()));
		List<NormalRule> transformedRules = inputProgram.getRules().stream()
				.map(rule -> containsModuleAtom(rule) ? linkModuleAtoms(rule, moduleTable) : rule)
				.collect(Collectors.toList());
		return Programs.newNormalProgram(transformedRules, inputProgram.getFacts(), inputProgram.getInlineDirectives(), Collections.emptyList());
	}

	private NormalRule linkModuleAtoms(NormalRule rule, Map<String, Module> moduleTable) {
		Set<Literal> newBody = rule.getBody().stream()
				.map(literal -> {
					if (literal instanceof ModuleLiteral) {
						ModuleLiteral moduleLiteral = (ModuleLiteral) literal;
						return translateModuleAtom(moduleLiteral.getAtom(), moduleTable).toLiteral(!moduleLiteral.isNegated());
					} else {
						return literal;
					}
				})
				.collect(Collectors.toSet());
		return Rules.newNormalRule(rule.getHead(), newBody);
	}

	private ExternalAtom translateModuleAtom(ModuleAtom atom, Map<String, Module> moduleTable) {
		if (!moduleTable.containsKey(atom.getModuleName())) {
			throw new IllegalArgumentException("Module " + atom.getModuleName() + " not found in module table.");
		}
		Module definition = moduleTable.get(atom.getModuleName());
		// verify inputs
		Predicate inputSpec = definition.getInputSpec();
		if (atom.getInput().size() != inputSpec.getArity()) {
			throw new IllegalArgumentException("Module " + atom.getModuleName() + " expects " + inputSpec.getArity() + " inputs, but " + atom.getInput().size() + " were given.");
		}
		NormalProgram normalizedImplementation = moduleRunner.normalizeProgram(definition.getImplementation());
		// verify outputs
		Set<Predicate> outputSpec = definition.getOutputSpec();
		Set<Predicate> expectedOutputPredicates;
		if (outputSpec.isEmpty()) {
			expectedOutputPredicates = calculateOutputPredicates(normalizedImplementation);
		} else {
			expectedOutputPredicates = outputSpec;
		}
		if (atom.getOutput().size() != expectedOutputPredicates.size()) {
			throw new IllegalArgumentException("Module " + atom.getModuleName() + " expects " + outputSpec.size() + " outputs, but " + atom.getOutput().size() + " were given.");
		}
		// create the actual interpretation
		PredicateInterpretation interpretation = terms -> {
			BasicAtom inputAtom = Atoms.newBasicAtom(inputSpec, terms);
			NormalProgram program = Programs.newNormalProgram(normalizedImplementation.getRules(),
					ListUtils.union(List.of(inputAtom), normalizedImplementation.getFacts()), normalizedImplementation.getInlineDirectives(), Collections.emptyList());
			java.util.function.Predicate<Predicate> filter = outputSpec.isEmpty() ? p -> true : outputSpec::contains;
			Stream<AnswerSet> answerSets = moduleRunner.solve(program, filter);
			if (atom.getInstantiationMode().requestedAnswerSets().isPresent()) {
				answerSets = answerSets.limit(atom.getInstantiationMode().requestedAnswerSets().get());
			}
			return answerSets.map(as -> answerSetToTerms(as, expectedOutputPredicates)).collect(Collectors.toSet());
		};
		return Atoms.newExternalAtom(atom.getPredicate(), interpretation, atom.getInput(), atom.getOutput());
	}

    [....]

	private static List<Term> answerSetToTerms(AnswerSet answerSet, Set<Predicate> moduleOutputSpec) {
		List<Term> terms = new ArrayList<>();
		for (Predicate predicate : moduleOutputSpec) {
			if (!answerSet.getPredicates().contains(predicate)) {
				terms.add(Terms.EMPTY_LIST);
			} else {
				terms.add(Terms.asListTerm(answerSet.getPredicateInstances(predicate).stream()
						.map(Atoms::toFunctionTerm).collect(Collectors.toList())));
			}
		}
		return terms;
	}


}

The actual translation step happens inside the method translateModuleAtom:

PredicateInterpretation interpretation = terms -> {
	BasicAtom inputAtom = Atoms.newBasicAtom(inputSpec, terms);
	NormalProgram program = Programs.newNormalProgram(normalizedImplementation.getRules(),
			ListUtils.union(List.of(inputAtom), normalizedImplementation.getFacts()), normalizedImplementation.getInlineDirectives(), Collections.emptyList());
	java.util.function.Predicate<Predicate> filter = outputSpec.isEmpty() ? p -> true : outputSpec::contains;
	Stream<AnswerSet> answerSets = moduleRunner.solve(program, filter);
	if (atom.getInstantiationMode().requestedAnswerSets().isPresent()) {
		answerSets = answerSets.limit(atom.getInstantiationMode().requestedAnswerSets().get());
	}
	return answerSets.map(as -> answerSetToTerms(as, expectedOutputPredicates)).collect(Collectors.toSet());
};
return Atoms.newExternalAtom(atom.getPredicate(), interpretation, atom.getInput(), atom.getOutput());

Here, we define the interpretation function for the newly-created external atom to be the result of calling moduleRunner.solve(....) for the program resulting from adding facts corresponding to the input terms of the module atom to the program constituting the module definition. moduleRunner is an instance of the Alpha solver that is used to run the program. The resulting ExternalAtom can the be evaluated like any other external atom, i.e. modularization is completely invisible to the grounder and solver components.

[1]: https://repositum.tuwien.at/handle/20.500.12708/220293 Michael Langowski. Evolog-Actions and Modularization in Lazy-Grounding Answer Set Programming. Master Thesis, Technische Universität Wien, 2025.