Fragment analysis

Logic programming allows for a broad range of reasoning tasks, some of which have big implications on how the program is computed: this can impact in particular decidability (if there exists an effective method for deriving the correct answer), termination (whether computation terminates or not), and computational complexity (the actual resource usage for solving a problem).

Vadacode constantly analyze your code in the background to highlight issues that could impede execution, helping you to write and fix your programs. Similarly to code diagnostics, the issues are shown inline with the usual squiggly line aesthetics and reported in the Problems tab of Visual Studio Code.

Vadacode implements several fragment-specific Diagnostic codes which detail whether rules, predicates or variables can be used safely.

When you install Vadacode, the status bar at the bottom of Visual Studio Code is enriched by a new selector:

The widget shows the currently active fragment, which is used to determine the set of diagnostics to apply to your code. By default, the fragment is set to Warded, which is the reference fragment for Vadalog. You can change the active fragment by clicking on the widget and selecting a different one from the quick-pick list that appears.

Active fragment is a per-workspace setting: you choose the fragment you want to work in, and the fragmentis applied to the diagnostics of all files in Vadalog projects.

Active fragment is stored in VSCode global state, so it’s kept after you close VSCode.

Vadacode supports the following fragments;

When selecting fragment, you can opt for Show all violations which enables all possible syntactic restrictions of supported fragments.

Similarly, Vadacode allows to select Datalog ∃ as the active fragment, which poses no restrictions on the use of the language and hence shows no fragment violations.

Warded Datalog±, a recent member of the Datalog family, is a special fragment for Vadacode team because it’s the core of the Vadalog language. In fact, the full Vadalog language is obtained as an extension to the Warded Datalog± core with features of practical utility (think i/o, aggregations, annotations, and so on).

The idea behind the notion of "wardedness" is taming the propagation of nulls during the construction of the answer in reasoning process. As this condition might be hard to evaluate in practice, Vadacode shows if it’s not met and marks the program elements which violate the needed assumption.

Warded Datalog± is described in [vadalog].

EGDs are an advanced feature of Vadalog that enables value-assignment or forcing the equivalence of fresh symbols. Essentially, it allows to constrain labeled nulls to have assigned the same values, yielding to the possibility to group new facts.

In general, an EGD has the form: X=Y :- body, where X and Y are two existential variables used in the body of the rule. In Vadacode, the equal sign is decorated with a Visual Studio Code hint indicating that it’s an EGD.

Nevertheless, admitting any kind of EGD in a Vadalog program would pose decidability issues, hence the introduction of harmless EGDs, a specific type of EGD under which ontological reasoning is decidable and PTIME; more specifically, an EGD is harmless if it respects a sufficient syntactic condition, namely "safe taintedness".

As this condition might be hard to evaluate in practice, especially in complex programs, Vadacode shows if this condition is not met with an error diagnostic.

Vadalog EGDs are described in [egd]. Vadacode supports EGD checks in the Warded Datalog± fragment.