/usr/share/mozart/doc/system/node16.html is in mozart-doc 1.4.0-8ubuntu1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD><TITLE>5.2 The Concept of Constructive Disjunction</TITLE><LINK href="ozdoc.css" rel="stylesheet" type="text/css"></HEAD><BODY><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="node15.html#section.fd.facts"><< Prev</A></TD><TD><A href="node14.html">- Up -</A></TD><TD><A href="node17.html#section.fd.general">Next >></A></TD></TR></TABLE><DIV id="section.fd.condis"><H2><A name="section.fd.condis">5.2 The Concept of Constructive Disjunction</A></H2><P>The operational semantics of some propagators is based on the concept of constructive disjunction which allows to lift common information from different clauses of a disjunctive constraint. </P><P>Constructive disjunction is <EM>not</EM> available as program combinator in Oz. Anyway, we use it in Oz program fragments (by the keyword <SPAN class="keyword"><CODE>condis</CODE></SPAN>) to describe the operational semantics of certain propagators. For example such propagators are <A href="node25.html#ref_tasksoverlap"><CODE>FD<SPAN class="keyword">.</SPAN>tasksOverlap</CODE></A> and <A href="node25.html#ref_disjoint"><CODE>FD<SPAN class="keyword">.</SPAN>disjoint</CODE></A>. </P><P>Constructive disjunction adopts the operational semantics of the nondistributable disjunction of Oz (<CODE><SPAN class="keyword">or</SPAN> <SPAN class="keyword">...</SPAN> <SPAN class="keyword">end</SPAN></CODE>) concerning entailment and failure of clauses. Furthermore, it extends the semantics as follows: Assume a disjunction with <I>n</I> clauses and let <I>S</I> be the constraint store of the computation space in which it resides. Let <IMG alt="S_1,\ldots,S_n" src="latex19.png"> denote the local stores of the <I>n</I> clauses. Then the strongest constraint <I>C</I> consisting of basic constraints <IMG alt="X\in D" src="latex20.png"> with <IMG alt="S_i\models C" src="latex21.png"> for <IMG alt="1\leq i
\leq n" src="latex22.png"> is lifted and added to <I>S</I>. </P><P>As an example consider the store <CODE>X<SPAN class="keyword">,</SPAN> Y</CODE><IMG alt="\in\{0,\ldots,10\}" src="latex23.png"> and </P><BLOCKQUOTE class="code"><SPAN class="keyword"><CODE>condis</CODE></SPAN><CODE> X <SPAN class="keyword">+</SPAN> 9 <SPAN class="keyword">=<:</SPAN> Y<BR><SPAN class="keyword">[]</SPAN> Y <SPAN class="keyword">+</SPAN> 9 <SPAN class="keyword">=<:</SPAN> X<BR><SPAN class="keyword">end</SPAN></CODE></BLOCKQUOTE><P> Constructive disjunction narrows the domains of <CODE>X</CODE> and <CODE>Y</CODE> to <IMG alt="\{0,1,9,10\}" src="latex24.png">.</P></DIV><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="node15.html#section.fd.facts"><< Prev</A></TD><TD><A href="node14.html">- Up -</A></TD><TD><A href="node17.html#section.fd.general">Next >></A></TD></TR></TABLE><HR><ADDRESS><A href="http://www.ps.uni-sb.de/~duchier/">Denys Duchier</A>, <A href="http://www.ps.uni-sb.de/~kornstae/">Leif Kornstaedt</A>, <A href="http://www.ps.uni-sb.de/~homik/">Martin Homik</A>, <A href="http://www.ps.uni-sb.de/~tmueller/">Tobias Müller</A>, <A href="http://www.ps.uni-sb.de/~schulte/">Christian Schulte</A> and <A href="http://www.info.ucl.ac.be/~pvr">Peter Van Roy</A><BR><SPAN class="version">Version 1.4.0 (20110908185330)</SPAN></ADDRESS></BODY></HTML>
|