Episteme - DML - Logical Constructions

Syntax of Logical Constructions

A construction is a sequence of steps that declare, reference, and operate on logical types. Each step takes prior knowledge, that which is given, and uses it to modify or do something to the current state of the construction. The syntax for declaring a construction takes the following form:

	<tei:div n='construction_num' type='proposition'>
	  <dialog:step n='step_num'>
	    <dialog:given>
	      <!-- one or more logical type declarations or refs -->
	    </dialog:given>
	    <dialog:do>
	      <!-- one or more type decls, refs, or operations -->
	    </dialog:do>
	  </dialog:step>
	 ... <!-- more steps may follow -->
	</tei:div>
      

Encoding Logical Constructions

Here is an excerpt from the second proposition of Archimedes' Floating Bodies, Book I.

	<tei:div n='3' type='proposition'>
	  <dialog:step n='step_num'>
	    <dialog:given>
	      <tlg1799.tlg001:point id='b'/>
	      <tlg1799.tlg001:straight_line id='ob'/>
	    </dialog:given>
	    <dialog:do>
	      <tlg1799.tlg001:circle id='ebf'>
	         <tlg1799.tlg001:point ref='o'/>
	         <tlg1799.tlg001:radius ref='ob'/>
	      </tlg1799.tlg001:circle>
	    </dialog:do>
	  </dialog:step>
	 ... <!-- more steps follow here -->
	</tei:div>	
      

Now that we know how to encode constructions, we can use them in other constructions! In some sense, a construction defines a function that takes zero or more logical primitives as input and produces one or more logical primitives as output. In this light, a construction resembles a logical operator. However, the construction also allows one to peek into the operator and see the state of its primitives change step-by-step. In this sense, one can view the construction as a collection of primitives constrained by the construction process.

Sometimes we may want to use multiple instances of the same construction in another construction. For this reason, we can gain access to the set of primitives at a given state of the construction by declaring a construction_instance

	<tei:div n='3' type='proposition'>
	  <dialog:step n='1'>
	    <dialog:given>
	      <dialog:construction_instance id='c2' ref='urn:dml:tlg0552.tlg008.logic01:2'/>
	    </dialog:given>
	    <dialog:do>
	      <tlg0552.tlg008:center_of_earth id='a' ref='c2:o'/>
	    </dialog:do>
	  </dialog:step>
	</tei:div>
      

The id attribute of the construction instance is used as an alias to the referenced DML-URN, the value in the ref attribute. The semantics of the DML-URN are very similar to that of the CTS-URN and more documentation on the DML-URN is pending. With this instance declared, I can now view the construction instance as a collection of primitives and use this id as a data namespace. This is precisely what is done when declaring center_of_earth a, the o logical primitive in construction instance c2 is referenced.