0
$\begingroup$

In Alloy Tutorial they denote some reflexive transitive closure with Kleene star saying that they admit zero or more elements at that position. 

  // File system is connected
  fact {
    FSObject in Root.*contents
  }

In Alloy, in can be read as "subset of" (among other things). The operator "*" denotes reflexive transitive closure. Thus, this fact says that the set of all file system objects is a subset of everything reachable from the Root by following the contents relation zero or more times.

Reflexive Transitive Closure *

In Alloy, "*bar" denoted the reflexive transitive closure of bar. It is equavalent to (iden + ^bar) where ^ is the (non-reflexive) transitive closure operator.

Can you explain the closure and star operators such thut it becomes obvious that they are identical?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

(Note: I'm not 100% sure about the Alloy syntax since I never used it -- what follows is accurate on the general principles but the syntax could be slightly different)

Basically, S.*bar means starting from S and using .bar any number $n\geq 0$ of times.

Instead, S.^bar means starting from S and using .bar any positive number $n > 0$ of times.

It is immediate to see that S.^bar is equivalent to S.bar.*bar since the latter denotes zero or more steps after a first step, hence one or more steps.

If the language allows S.iden to mean "zero steps from S", and + to denote union, then we can also write S.^bar as S.(iden + ^bar) which can be read as "zero steps or (one step or more)" which is the same thing as "zero or more steps".

In the underlying theory, one can define the reflexive and transitive closure of a relation $R \in \mathcal{P}(A\times A)$ as the smallest relation $R^* \in \mathcal{P}(A\times A)$ satisfying

$$ R^* = I_A \cup R \circ R^* $$

where $I_A$ stands for the identity relation. The existence of the smallest $R^*$ is guaranteed by the Tarski fixed point theorem (on the complete lattice of the relations). According to the Kleene fixed point theorem (and a few minor simplifications) one can also write it as $$ R^* = \bigcup_{n\geq 0} R^n $$ where $R^n$ denoted the self-composition of $R$ for $n$ times.

Improve this answer
$\endgroup$
3
  • $\begingroup$ In $R^* = I_A \cup R \circ R^*$, do you define the relation in terms of itself? Is your purpose is to show that $\bigcup_{n\geq 0} R^n = I_A \cup R \circ R^*$? Can you reduce it into more layman terms? $\endgroup$
    – Little Alien
    Commented Dec 29, 2016 at 13:57
  • $\begingroup$ @LittleAlien I corrected the first part: it is indeed zero or more. For the latter part, if you want to be informal, you can pretend that $R^*$ is defined in terms of itself as $I \cup R\circ R^*$ (or pretend that the definition is recursive). The truth is the equation $R^* = I \cup R\circ R^*$ might have multiple solutions for $R^*$, and we take the smallest one. The underlying theory is quite broad (you can look up fixed point theorems or domain theory), and I can't summarize it here. However, $R^* = \bigcup_n R^N$ provide its smallest solution in a convenient form, in layman terms. $\endgroup$
    – chi
    Commented Dec 29, 2016 at 14:12
  • $\begingroup$ @LittleAlien From $R^* = \bigcup_{n\geq 0} R^n = I \cup R \cup R\circ R\ \cup \cdots$ you can see that the solution is indeed "zero or more times" $R$. $\endgroup$
    – chi
    Commented Dec 29, 2016 at 14:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.