User:Jochen Burghardt/sandbox

This is the user sandbox of Jochen Burghardt. A user sandbox is a subpage of the user's user page. It serves as a testing spot and page development space for the user and is not an encyclopedia article. Create or edit your own sandbox here.

Other sandboxes: Main sandbox | Template sandbox

Finished writing a draft article? Are you ready to request review of it by an experienced editor for possible inclusion in Wikipedia? Submit your draft for review!

NuSMV

MODULE main
VAR
  semaphore : boolean;
  proc1 : process user(semaphore);
  proc2 : process user(semaphore);
ASSIGN
  init(semaphore) := FALSE;
SPEC
  AG (proc1.state = entering -> AF proc1.state = critical)

MODULE user(semaphore)
VAR
  state : {idle,entering,critical,exiting};
ASSIGN
  init(state) := idle;
  next(state) :=  
    case 
      state = idle : {idle,entering};
      state = entering & !semaphore : critical;
      state = critical : {critical,exiting};
      state = exiting : idle;
      TRUE : state;
    esac;
  next(semaphore) :=  
    case
      state = entering : TRUE;
      state = exiting : FALSE;
      TRUE : semaphore;
    esac;
FAIRNESS
  running

Distributive elements

In a (distributive or non-distributive) lattice, an element x is called a distributive element if ∀y,z: x ∨ (y ∧ z) = (x ∨ y) ∧ (x ∨ z). An element x is called a dual distributive element if ∀y,z: x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z). In a distributive lattice, every element is both distributive and dual distributive. In a non-distributive lattice, there may be elements that are distributive, but not dual distributive, and vice versa. For example, in the depicted pentagon lattice N₅,

Rational consequence relation

In classical logic, a statement^{[note 1]} $\theta \vdash ^{*}\phi$ implies the statement $\theta \wedge \psi \vdash ^{*}\phi$ under all circumstances. For example, the statement

"If a cake contains sugar then it tastes good", formally ${\text{isCake}}(x)\land {\text{contains}}(x,{\text{sugar}})\vdash ^{*}{\text{delicious}}(x)$ ,

implies under a monotone consequence relation the statement

"If a cake contains sugar and soap then it tastes good", ${\text{isCake}}(x)\land {\text{contains}}(x,{\text{sugar}})\land {\text{contains}}(x,{\text{soap}})\vdash ^{*}{\text{delicious}}(x)$ .

Clearly this doesn't match our own understanding of cakes. Non-monotonic logic, in particular the rational consequence relation, is designed to avoid this undesired inference. By asserting

"If a cake contains sugar then it usually tastes good", ${\text{isCake}}(x)\land {\text{contains}}(x,{\text{sugar}})\vdash {\text{delicious}}(x)$ ,

a rational consequence relation allows for a more realistic model of the real world, and it does not automatically follow that

"If a cake contains sugar and soap then it usually tastes good", ${\text{isCake}}(x)\land {\text{contains}}(x,{\text{sugar}})\land {\text{contains}}(x,{\text{soap}})\vdash {\text{delicious}}(x)$ .

However, in some cases, we do want to conclude $\theta \wedge \psi \vdash \phi$ from $\theta \vdash \phi$ . Rules CMO and RMO serve that purpose; we give an example how each of them can be applied. If we also have the information

"If a cake contains sugar then it usually contains butter", ${\text{isCake}}(x)\land {\text{contains}}(x,{\text{sugar}})\vdash {\text{contains}}(x,{\text{butter}})$ ,

then we may legally conclude, under CMO, that

"If a cake contains sugar and butter then it usually tastes good", ${\text{isCake}}(x)\land {\text{contains}}(x,{\text{sugar}})\land {\text{contains}}(x,{\text{butter}})\vdash {\text{delicious}}(x)$ .

Using rule RMO,

"If a cake contains sugar then usually it contains no soap", ${\text{isCake}}(x)\land {\text{contains}}(x,{\text{sugar}})\vdash \lnot {\text{contains}}(x,{\text{soap}})$

then we could legally conclude from RMO that

"If the cake contains sugar and soap then it usually tastes good", ${\text{isCake}}(x)\land {\text{contains}}(x,{\text{sugar}})\land {\text{contains}}(x,{\text{soap}})\vdash {\text{delicious}}(x)$ .

If this latter conclusion seems ridiculous to you then it is likely that you are subconsciously asserting your own preconceived knowledge about cakes when evaluating the validity of the statement. That is, from your experience you know that cakes that contain soap are likely to taste bad so you add to the system your own knowledge such as "Cakes that contain sugar do not usually contain soap.", even though this knowledge is absent from it. If the conclusion seems silly to you then you might consider replacing the word soap with the word eggs to see if it changes your feelings.

Relation (mathematics)

Excerpt from the Curie family tree

Properties of, and operations on, mathematical relations can be explained along family relationships.

The relation "is a child of" is

irreflexive (nobody is a child of her/himself),
asymmetric (if x is a child of y, then y cannot be a child of x),
right-total (everybody is the child of someone),
but not left-total (not everybody has a child).

The relation "is a decendant of" is

antisymmetric (if x is a decendant of y, then y cannot be a decendant of x),
transitive (if x is a descentant of y, and y is a descendant of z, then x is also a descendant of z),
right-total (everybody is descendant of someone).

Different conventions may be adopted as to whether it is reflexive ("everybody is considered a descendant of her/himself"), irreflexive ("nobody is considered a descendant of her/himself"), or possibly even none of both ("some people are considered a descendant of her/himself, while others are not").

The relation "is a parent of" is the converse of "is a child of": x is a parent of y if, and only if, y is a child of x. Therefore, "is a parent of" is

irreflexive (nobody is a parent of her/himelf, since -see above- nobody is a child of her/himself),
asymmetric (if x is a parent of y, then y is a child of x, hence -see above- x cannot be a child of y, that is, y cannot be a parent of x),
left-total (everybody has a parent, since -see above- everybody is the child of someone),
but not right-total (not everybody is the parent of somebody, since -see above- not everybody has a child).

The relation "is a child of" is the union of "is a daughter of" and "is a son of":^{[note 2]} x is a child of y if, and only if, x is a daughter of y, or x is a son of y.

The relation "is an aunt of" is the composition of "is a parent of" ∘ "is a sister of": x is an aunt of z if, and only if, x is a sister of some y such that y is a parent of z. For example, Bronisława Dłuska is an aunt of Ève Curie, since Bronisława Dłuska is a sister of Marie Curie, which, in turn, is a parent of Ève Curie, cf. picture.

Composing in reverse order yields a different relation R:^{[note 3]} we have x R z if, and only if, x is a parent of some y such that y is a sister of z. While R is contained in the relation "is a parent of", both relations do not coincide: for example, Anne Joliot [fr] is a parent of Marc Joliot, but (Anne Joliot)R(Marc Joliot) does not hold as long as Marc Joliot does not have a sister.

TO DO: illustrate Intersection, Complement, Restriction
TO DO: illustrate all Combinations of properties
TO DO: illustrate properties Connected

Recent

In particular, a definition an intended function f may establish a relation that is not right-unique or not serial, and hence in fact not a function. In that case, f is called ill defined; if it is not right-serial, f is also called ambiguous.

commons:User:Jochen Burghardt

Relation (mathematics)


q p	1	2	3	4	5	6
1
2
3
4
5
6
Relation $R_{2}$ : Value p divides value q


q p	1	2	3	4	5	6
1
2
3
4
5
6
Relation $R_{1}$ : Face p adjacent to face q



Example die

In mathematics, a relation on a set $X$ associates certain elements of $X$ with each other. Formally, a relation $R$ on $X$ is a set of ordered pairs of elements of $X,$ that is, a subset of the Cartesian product $X\times X$ . An element $x$ of $X$ is related to an element $y$ if the pair $(x,y)$ is an element of $R$ .

For example, "is adjacent to" is a relation on the set of faces of the depicted example die; it associates e.g. 5,6, and likewise 6,3, but neither 3,4, nor 1,6. The left table shows for each cell whether its row's face is adjacent to its column's face. The example adjacency relation is represented as the set

{\begin{array}{lcccc}R_{1}=\{&(1,2),&(1,3),&(1,4),&(1,5),\\&(2,1),&(2,3),&(2,4),&(2,6),\\&(3,1),&(3,2),&(3,5),&(3,6),\\&(4,1),&(4,2),&(4,5),&(4,6),\\&(5,1),&(5,3),&(5,4),&(5,6),\\&(6,2),&(6,3),&(6,4),&(6,5)&\};\\\end{array}}

this set has one element for each " " entry in the left table.

Another relation example on the same set is "divides"; it associates e.g. 3,6, but not 6,3. The right table illustrates this relation. Its is represented as the set

{\begin{array}{lccccc}R_{2}=\{&(1,1),&(1,2),&(1,3),&(1,4),&(1,5),\\&(2,2),&(2,4),&(2,6),&(3,3),&(3,6),\\&(4,4),&(5,5),&(6,6)&&&\};\\\end{array}}

again, this set has one element for each " " entry in the right table.

Equation

Well, Variety_(universal_algebra) link to identity (mathematics), which gives a fairly usable definition in its first sentence, viz. "An identity is an equality relating one mathematical expression A to another mathematical expression B, such that A and B (which might contain some variables) produce the same value for all values of the variables within a certain range of validity". I'd formalize this as: "An identity of a formula of the form ∀x₁,...,x_n. s = t, where s and t are terms with no other free variables than x₁,...,x_n". An example identity set is { ∀x,y,z.x*(y*z)=(x*y)*z , ∀x. x*1=x } for the theory of monoids. The quantifier prefix is often omitted, like { x*(y*z)=(x*y)*z , x*1=x } in the example.

In English Wikipedia, at least the articles "identity (mathematics)", "equality (mathematics)", and "equation" deal with this issue; they mainly differ by the purpose a formula is used for. "Identity" and "equality" (I believe there is no difference between these concepts) take the formula as an assertion from which other formulas may be inferred, while "equation" takes the "s=t" part as something to be solved (like x²-2x+1=0); more formally, a constructive proof is sought for ∃x₁,...,x_n. s = t. However, none of the 3 articles mentions quantification at all.

Table in footnote ref

Main subsection

Main^[1] text^[2] blah blah.^[3]

References subsection

^ Previous footnote
^ Footnote with table: start here

English translation German text

left right

end here.
^ Next footnote

Next subsection

Text in next subsection.

Set constraint

Different approaches admit different operators on sets, cf. table.

Bachmair, Ganzinger, Waldmann (1992)	{}	U	X	E₁ ∪ E₂	E₁ ∩ E₂	U \ E₁	f(E₁,...,E_n)	E₁ ⊆ E₂	E₁ = E₂
Regular tree grammars			X	E₁ ∪ E₂			f(E₁,...,E_n)		E₁ = E₂

U: Universe, X: Variable, E_i: sub-expression

Markup / template examples

blue on red

A link to the lead of this page

Reference within note: Chaplin believed he was born in South London.^{[note 4]}

Reference within reference: linear indexed grammars,^[5] By requiring^[3] ... ^[5]

Notes

^ We use $\vdash ^{*}$ here to denote the classical consequence relation (informally: "If ... then always ..."). In constrast, we use $\vdash$ to denote the rational consequence relation (informally: "If ... then usually ...").
^ In a non-binary setting, "is a child of" is the union of more than two relations, one for each gender.
^ Similar to child relations for non-binary genders, there is no traditional relation name available, so we use just R.
^ Outer reference (template): record ^[1] Date of his birth.^[2] End of outer reference

References

^ Inner reference (markup): "Thornstein". The Telegraph. 17 February 2012. Retrieved 11 April 2012. End of inner reference
^ Robinson, p. xxiv.
^ ^a ^b staudacher1993
^ Weir (1988). "Grammars". Proc. pp. 278–285.
^ ^a ^b According to Staudacher (1993, p.361 left, Sect.2.2),^[3] the name.^[4]

[4] Previous footnote

[5] Footnote with table: start here

English translation German text

left right

end here.

[6] Next footnote

[1] We use $\vdash ^{*}$ here to denote the classical consequence relation (informally: "If ... then always ..."). In constrast, we use $\vdash$ to denote the rational consequence relation (informally: "If ... then usually ...").

[2] In a non-binary setting, "is a child of" is the union of more than two relations, one for each gender.

[3] Similar to child relations for non-binary genders, there is no traditional relation name available, so we use just R.

[9] Outer reference (template): record ^[1] Date of his birth.^[2] End of outer reference

[7] Inner reference (markup): "Thornstein". The Telegraph. 17 February 2012. Retrieved 11 April 2012. End of inner reference

[8] Robinson, p. xxiv.

[staudacher1993-10] staudacher1993

[11] Weir (1988). "Grammars". Proc. pp. 278–285.

[outer2-12] According to Staudacher (1993, p.361 left, Sect.2.2),^[3] the name.^[4]

[note 1]

[note 2]

[note 3]

[1]

[2]

[3]

[note 4]

[5]

[3]

[1]

[2]

[4]