Error in the code generator for singletons

[stefjoosten]

What happened

I ran the following Ampersand script for the purpose of demonstrating that the rule UniverseExists guarantees that the atom _UNIVERSE of type Module always exists.

CONTEXT Issue1475
RELATION id[Module*Id] [UNI,TOT]
INTERFACE Modules FOR User: "_SESSION";V[SESSION*Module] BOX [ id : id ]
RULE UniverseExists : "_UNIVERSE" |- I[Module]
POPULATION id CONTAINS [ ("_UNIVERSE", "_UNIVERSE") ]
ENDCONTEXT

I executed the prototype. To my surprise, I found that I can delete module _UNIVERSE in the most straightforward way:

Screen.Recording.2024-03-29.at.07.26.14.mov

What I expected

I expected that the prototype would not let me delete module _Universe. Just to verify, I compiled the script without the population statement. As expected I got a compiler message that noticed the missing module:

.246 /usr/local/project/Issue1475.adl:4:1 error:
0.246   There is one violation of RULE "UniverseExists":
0.247     ("_UNIVERSE", "_UNIVERSE")
0.247 2024-03-29 07:01:05.852413: [error] ExitFailure 10

This confirms my expectation that the back end should not allow me to delete module _UNIVERSE.

Version of ampersand that was used

I ran the prototype on ampersandtarski/prototype-framework:v1.14, which runs Ampersand-v4.6.2 [51c3de2:refs/tags/v4.6.2] with the following settings: --[no-]backend True --[no-]frontend True --[no-]metamodel False --[no-]terminal False --[no-]time-in-log True --[no-]trim-cellvalues True --build-recipe Prototype --crud-defaults CRUD --frontend-version AngularJS --ignore-invariant-violations False --interfaces False --language Nothing --namespace "" --output-dir "." --proto-dir "/var/www" --sql-bin-tables False --terminal-width Nothing --verbosity debug

[hanjoosten]

This again seems a case of the Sinterklaas issue.
The rule you expect to be violated is:

RULE UniverseExists : "_UNIVERSE"[Module] |- I[Module]

This rule can NEVER be violated.

[hanjoosten]

You might give the following rule a try:

ENFORCE -"_UNIVERSE"[Module] |- "_UNIVERSE"[Module]

[hanjoosten]

Diagnosis

The compiler generates the following SQL-fragment for computing the violations:

select distinct t1.src as src, t1.tgt as tgt 
from (select "Module" as src, "Module" as tgt 
      from "Module" where "Module" = '_UNIVERSE') as t1 
              left join 
     (select "Module" as src, "Module" as tgt from "Module" 
              where "Module" is not null) as t2
              on (t1.src = t2.src) and (t1.tgt = t2.tgt) 
where (t2.src is null) or (t2.tgt is null)

This explains the runtime behavior because t1 will be empty.

[stefjoosten]

An alternative way to write the fact that the universe exists might be:

RULE UniverseExists : "_UNIVERSE"[Module]

@sjcjoosten , would this be a correct rule in your opinion?
The compiler wants it to be the only atom in Module, because it comes back with the following error message, after I took a second module Foo in the population:

0.263 /usr/local/project/modules.adl:205:1 error:
0.263   There are 3 violations of RULE "UniverseExists":
0.263     ("Foo", "Foo")
0.263     ("Foo", "_UNIVERSE")
0.263     ("_UNIVERSE", "Foo")
0.263 2024-03-30 10:45:51.621869: [error] ExitFailure 10

[hanjoosten]

I had a call with @stefjoosten . I mentioned the rule

$$r ; I = I ; r = r$$

In Ampersand, at runtime we have our population in a database, and we check that population for violations of rules. So if we speak about a violation, we actually say that the content of the database violates that rule.

Any expression may be used as the expression of a rule. So to check that "_UNIVERSE" exists in our population, we need a properly typed expression: "_UNIVERSE"[Module]. This expression can be used as the formal expression of a rule:

RULE UniverseExists : "_UNIVERSE"[Module]

This must be translated into an SQL expression that checks for violations in the database. It must return nothing if "_UNIVERSE" exists in the concept Module. But what should it return if "_UNIVERSE" is missing??

[hanjoosten]

About finding violations

To find violations of some expression expr, we look for differences between what we find in the population (the database) and tuples in the expression. In this case, that is

$$\{ (x,y) | x \in Module, y \in Module, (x,y) \notin ('\_UNIVERSE','\_UNIVERSE') \}$$

This is exactly what is returned as violations, but is not what you intended.

Maybe we need a new operator for this intention?

[hanjoosten]

Or the rule should be defined something like:

RULE newAttempt : V[Module] ; "_UNIVERSE" ; V[Module]

[hanjoosten]

I have done some more thinking on this issue. The newAttempt rule above doesn't do the job, for if there aren no modules at all, there is no violation detected, which contradicts with Stef's intention.
If the population is empty, no violations will be reported, because the difference between what we find in the population (the database) and tuples in the expression will be empty. Hence no violations.

Fortunately, the population must never be empty, because ONE[ONE] is there by definition. At least, a proper implementation of Ampersand must guarantee that. If we take this into account, a true way to express Stef's intention will be:

RULE universeExistsDoneProperly : V[ONE*Module]; "_UNIVERSE" ; V[Module*ONE]

Currently, I believe it is possible to remove ONE[ONE] from the population. That should be fixed by fixing the translation of expression to SQL to let that SQL not inspect the database for it, but merely translate it to

select "ONE" as "ONE";

[RieksJ]

I recently made a demo where to my surprise ONE could be deleted, similarly to what Stef stated in his initial post.