Difference between pages "D23 Code Generation" and "Membership in Goal"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Pascal
 
imported>Billaude
 
Line 1: Line 1:
=Overview and Motivation=
+
= Objective =
  
Code generation is an important part of the formal engineering tool chain that will enable complete support for development from high-level models down to executable implementations. Work has commenced on the development of support for code generation from Event-B models. This is a new line of work for DEPLOY that was not identified in the original Description of Work for the project.  During the first year of the project, as the Deployment Partners gained experience with deployment of formal modelling, it became clear that having support for generation of code from refined Event-B models would be an important factor in ensuring eventual deployment of the DEPLOY approach within their organisations.  This is especially true for Bosch and Space Systems Finland (SSF).  During the DEPLOY re-focus at Month 18, it was decided to introduce a code generation task into a revised workplan and devote resources to this task.
+
This page describes the design of the reasoner MembershipGoal and its associated tactic MembershipGoalTac.<br>
 +
This reasoner discharges sequent whose goal denotes a membership which can be inferred from hypotheses. Here an basic example of what it discharges :<br>
 +
<math>H,\quad x\in S,\quad S\subset T,\quad T\subseteq U \quad\vdash x\in U</math>
  
After receiving more detailed requirements from Bosch and SSF, it became clear we should focus our efforts on supporting the generation of code for typical real-time embedded control software.  In essence, this involves programs structured as tasks running concurrently such as supported by the Ada tasking model.  The individual tasks are sequential programs and tasks share state variables via some form of monitor mechanism.  For real-time control, both periodic and aperiodic task should be supported; tasks should have priorities to ensure appropriate responsiveness of the control software.
+
= Analysis =
  
For the DEPLOY pilots, it is regarded as sufficient to support construction of programs with a fixed number of tasks and a fixed number of shared variables – no dynamic creation of processes or objects is required. It is not our intention to develop a fully-fledged industrial-strength code generation framework within the lifetime of the DEPLOY projectInstead an aim is to develop a sufficient framework to act as a proof-of-concept to enable code generation for the Bosch and SSF pilots.  A further aim is to gain practical experience with a prototype code generation framework that will serve as a basis for future R&D on a scalable code generation framework.
+
Such sequent are proved by PP and ML. But, these provers have both drawbacks :
The code generation work is being lead by Southampton with initial input from Newcastle.
+
*All the visible are added as needed hypotheses, which is most of the time not the case.
 +
*They take quite consequent time to prove it (even with the basic example given here above, the difference in time execution is noticeable).
 +
*If there are too many hypotheses, or if the expression of the <math>x</math> is too complicated, they may not prove it.
 +
This is particularly true when in the list of inclusion expressions of each side of the relation are not equal. For example : <math>H,\quad a\in S,\quad S\subset T_1\cap T_2,\quad T_1\cup T_3\subseteq U\quad\vdash a\in U</math>
 +
<p>
 +
Such a reasoner contributes to prove more Proof Obligations automatically, faster and with fewer needed hypotheses which makes proof rule more legible and proof replay less sensitive to modifications.
  
=Choices / Decisions=
+
= Design Decision =
Three candidate approaches have been posited as follows:
 
* Enrich Event-B with explicit algorithmic structures for use in later refinement stages and use these explicit structures to guide code generation.
 
* Synthesise sequential and concurrent code from existing low-level Event-B models.
 
* Exploit the code generation facilities of Atelier-B for “classical” B.
 
  
Approach 3 will be important for STS in WP2 as it will enable integration of Rodin with the existing development process in STS with AtelierB and some effort will be devoted to this.  However, this approach will not address the needs of all the deployments because of the overhead involved in having to use AtelierB alongside Rodin as well as the lack of support for concurrent code generation in AtelierB.  Supporting Approach 2 has the attraction that developers can remain within the uniform language framework of Event-B.  However, it is not clear that we can meet the real-time performance guarantees required for embedded systems with this approach within the lifetime of the DEPLOY project. 
+
== Tactic ==
  
While we will pursue some exploration of this approach, we will focus most effort on Approach 1 as this will enable existing techniques for real-time programming to be incorporated in later stages of development. Language support for explicit sequential and concurrent programs will be defined to enable construction of code-oriented models at low levels of refinement. We refer to this form of Event-B as task-oriented. A code generation framework will be developed to enable automated generation of C and Ada subsets suitable for real-time embedded systems from code-oriented models. A refinement-based proof method for code-oriented models will be defined and incorporated into the Rodin toolset.
+
This part explains how the tactic (MembershipGoalTac) associated to the reasoner MembershipGoal is working.
 +
=== Goal ===
 +
The tactic (as the reasoner) should works only on goals such as :
 +
*<math>\cdots~\in~\cdots</math>
 +
For examples :
 +
*<math>f(x)\in g\otimes h</math>
 +
*<math>x\in A\cprod\left(B\cup C\right)</math>
 +
*<math>x\mapsto y\in A\cprod B</math>
 +
In the latter case, the reasoner won't try to prove that ''x'' belongs to ''A'' and ''y'' belongs to ''B'', but that the mapplet belong to the Cartesian product.
 +
=== Hypotheses ===
 +
Now we have to find hypotheses leading to discharge the sequent. To do so, the tactic recovers two kinds of hypotheses :
 +
#the ones related to the left member of the goal <math>\left( x\in S\right)</math> (this is the start point):
 +
#*<math>x\in \cdots</math>
 +
#*<math>\cdots\mapsto x\mapsto\cdots\in\cdots</math>
 +
#*<math>\left\{\cdots, x,\cdots\right\}=\cdots</math>
 +
#*<math>\left\{\cdots, \cdots\mapsto x\mapsto\cdots,\cdots\right\}=\cdots</math>
 +
#the ones denoting inclusion (all but the ones matching the description of the first point) :
 +
#*<math>\cdots\subset\cdots</math>
 +
#*<math>\cdots\subseteq\cdots</math>
 +
#*<math>\cdots=\cdots</math>
 +
Then, it will search a link between those hypotheses so that the sequent can be discharged.
 +
=== Find a path ===
 +
Now that we recovered all the hypotheses that could be useful for the reasoner, it remains to find a path among the hypotheses leading to discharge the sequent. Depending on the relations on each side of the inclusion, we will act differently. <math>f</math> always represent an expression (may be a domain, a range, etc.).
 +
#The following sequent is provable because <math>f\subseteq \varphi (f)</math>.
 +
#*<math>x\in f,\quad \varphi (f)\subseteq g\quad\vdash\quad x\in g</math>
 +
#*<math>\varphi (f) = f\quad\mid\quad f\cup h \quad\mid\quad h\cup f \quad\mid\quad h\ovl f</math>
 +
#The following sequent is provable because <math>\psi (f)\subseteq f</math>.
 +
#*<math>x\in \psi (f),\quad f\subseteq g\quad\vdash\quad x\in g</math>
 +
#*<math>\psi (f) = f\quad\mid\quad f\cap h \quad\mid\quad h\cap f \quad\mid\quad f\setminus h \quad\mid\quad f\ransub A \quad\mid\quad f\ranres A \quad\mid\quad A\domsub f \quad\mid\quad A\domres f</math>
 +
#We can generalized the first two points. This is the Russian dolls system. We can easily prove a sequent with multiple inclusions by going from hypothesis to hypothesis.
 +
#*<math>x\in \psi (f),\quad \varphi (f)\subseteq g\quad\vdash\quad x\in g</math>
 +
#For some relations, [[#positions|positions]] are needed to be known to continue to find hypotheses, but it is not always necessary.
 +
#*<math>x\mapsto y\in f,\quad f\subseteq A\cprod B\quad\vdash\quad x\in A</math>
 +
#*<math>x\in dom(f),\quad f\subseteq A\cprod B\quad\vdash\quad x\in A</math>
 +
#*<math>x\in ran(f),\quad f\subseteq A\cprod B\quad\vdash\quad x\in B</math>
  
An important requirement is that the code generation framework be amenable to extension and tailoring for specific needs.  Rather than hard-wiring the code generation rules into the tool, we will aim to support a declarative rule-based approach to defining translation from task-oriented Event-B to a target implementation language. The translation should be tailorable by modifying or extending the declarative translation rules. We will explore the use of a model-based transformation framework such as ATL or ETL for this purpose.  Rather than fixing on a specific set of implementation-level data types, we will exploit the mathematical extension facility being developed for Rodin to enable a flexible approach to defining implementation-level data structures. For example, arrays could be supported by defining a new theory of arrays.  This theory would define array declarations and operators along with an appropriate set of proof rules for arrays to enable reasoning.  Appropriate declarative rules would then be defined to translate array declarations and expressions to appropriate code in the target language.
+
By using these inclusion and rewrites, it tries to find a path among the recovered hypotheses. Every one of those should only be used once, avoiding possible infinite loop <math>\left(A\subseteq B,\quad B\subseteq A\right)</math>. Among all paths that lead to discharge the sequent, the tactic give the first it finds. Moreover, so that the reasoner does not do the same work as the tactic of writing new hypothesis, it gives all needed hypotheses and added hypotheses in the input.
  
=Tasking Language=
+
== Reasoner ==
The Event-B tasking language will support the following sequential and concurrent algorithmic constructs:
 
{| border="1"
 
|Behaviour
 
|Algorithmic Construct
 
|-
 
|Sequence
 
|;
 
|-
 
|Branching
 
|if
 
|-
 
|Iteration
 
|while
 
|-
 
|Task/Thread/Process
 
|task
 
|-
 
|Shared variables
 
|machine
 
|}
 
  
A task-oriented model will be definable using the following abstract syntax
+
The way the reasoner must work is still in discussion.
{| border="0"
 
|Task := 
 
|-
 
|
 
| '''task'''  Name 
 
|-
 
|
 
| '''variables''' Variables
 
|-
 
|
 
| '''invariants''' Invariants 
 
|-
 
|
 
| '''begin''' TaskBody  '''end'''
 
|}
 
  
{| border="0"
+
= Implementation =  
| TaskBody :=  
 
|-
 
|
 
| Event
 
|-
 
|
 
|  <math>|</math> TaskBody  ;  TaskBody
 
|-
 
|
 
|  <math>|</math> '''if'''    Guard→ TaskBody  []  … []  Guard→ TaskBody  '''fi'''
 
|-
 
|
 
|  <math>|</math> '''do'''  Guard→ TaskBody  []  … []  Guard→ TaskBody  '''od'''
 
|}
 
  
The sequence, branching and iteration constructs correspond to their imperative counterparts. The task construct provides a means to specify the actions of interleaving, concurrent executions. A task may be implemented by an Ada task, or a thread in C.  A task, in isolation, is a sequential program with clearly identified atomic steps, and each step corresponding to an atomic event.  
+
This section explain how the tactic has bee implemented.
  
The standard machine construct provides the mechanism for sharing data between the executing tasks. The interaction between a task and a machine can be represented synchronized event composition as currently supported by the synchronised-event plug-in. The generated implementation will need to ensure that a task has mutually exclusive access to the variables represented in the machine. This is provided by a machine’s atomic events. A machine representing shared variables may be implemented by an Ada protected object, or in C by an explicit Mutex variable and appropriate lock acquisition.  
+
=== Positions ===
 +
As it was said, we may sometimes need the position. It is represented by an array of integer. Here are the possible values the array contains (atomic positions) :
 +
* '''''kdom''''' : it corresponds to the domain.
 +
**<math>\left[A\cprod B\right]_{pos\;=\;kdom} = A</math>
 +
**<math>\left[x\mapsto y\right]_{pos\;=\;kdom} = x</math>
 +
**<math>\left[g\right]_{pos\;=\;kdom} = dom(g)</math>
 +
* '''''kran''''' : it corresponds to the domain.
 +
**<math>\left[A\cprod B\right]_{pos\;=\;kran} = B</math>
 +
**<math>\left[x\mapsto y\right]_{pos\;=\;kran} = y</math>
 +
**<math>\left[g\right]_{pos\;=\;kran} = ran(g)</math>
 +
* '''''leftDProd''''' : it corresponds to the left member of a direct product.
 +
**<math>\left[f\otimes g\right]_{pos\;=\;leftDProd} = f</math>
 +
**<math>\left[A\cprod \left(B\cprod C\right)\right]_{pos\;=\;leftDProd} = A\cprod B</math>
 +
* '''''rightDProd''''' : it corresponds to the right member of a direct product
 +
**<math>\left[f\otimes g\right]_{pos\;=\;rightDProd} = g</math>
 +
**<math>\left[A\cprod\left(B\cprod C\right)\right]_{pos\;=\;rightDProd} = A\cprod C</math>
 +
* '''''leftPProd''''' : it corresponds to the left member of a parallel product
 +
**<math>\left[f\parallel g\right]_{pos\;=\;leftPProd} = f</math>
 +
**<math>\left[\left(A\cprod B\right)\cprod\left(C\cprod D\right)\right]_{pos\;=\;leftPProd} = A\cprod C</math>
 +
* '''''rightPProd''''' : it corresponds to the right member of a parallel product
 +
**<math>\left[f\parallel g\right]_{pos\;=\;rightPProd} = g</math>
 +
**<math>\left[\left(A\cprod B\right)\cprod\left(C\cprod D\right)\right]_{pos\;=\;rightPProd} = B\cprod D</math>
 +
* '''''converse''''' : it corresponds to the child of an inverse
 +
**<math>\left[f^{-1}\right]_{pos\;=\;converse}=f</math>
 +
**<math>\left[A\cprod B\right]_{pos\;=\;converse} = B\cprod A</math>
 +
For example, the following expressions at the given positions are equivalent.
 +
:<math>\left[f\otimes\left(\left(A\cprod dom(g)\right)\parallel g\right)\right]_{pos\;=\;\left[rightDProd,\;leftPProd,\;kran\right]} = \left[\left(A\cprod dom(g)\right)\parallel g\right]_{pos\;=\;\left[leftPProd,\;kran\right]} = \left[A\cprod dom(g)\right]_{pos\;=\;\left[kran\right]} = \left[dom(g)\right]_{pos\;=\;\left[~\right]} = \left[g\right]_{pos\;=\;\left[kdom\right]}</math>
  
To facilitate real-time programming constructs, we introduce the notion of task type, task period, and task priority.
+
Some combinations of atomic positions are equivalent. In order to simplify comparison between positions, they are normalized :
{| border="0"
+
*<math>ran(f^{-1}) = dom(f)\quad\limp\quad \left[f\right]_{pos \;=\; \left[converse,~kran\right]} = \left[f\right]_{pos\;=\;\left[kdom\right]}</math>
|Task :=  
+
*<math>dom(f^{-1}) = ran(f)\quad\limp\quad \left[f\right]_{pos \;=\; \left[converse,~kdom\right]} = \left[f\right]_{pos\;=\;\left[kran\right]}</math>
|-
+
*<math>\left(f^{-1}\right)^{-1} = f\quad\limp\quad \left[f\right]_{pos \;=\; \left[converse,~converse\right]} = \left[f\right]_{pos\;=\;\left[~\right]}</math>
|
 
| '''task'''  Name 
 
|-
 
|
 
| '''tasktype''' '''periodic'''(p) <math>|</math> '''triggered''' <math>|</math> '''repeating''' <math>|</math> '''oneshot'''
 
|-
 
|
 
| '''priority''' n
 
|-
 
|
 
| ...
 
|}
 
  
A tasktype is used to indicate the scheduling requirements for the required activity.  It is typically the case in real-time systems that the required activity involves some repeating behaviour, this can be a continuously repeating loop, or one that repeats at a predetermined time interval. We introduce repeating and periodic tasktypes. The periodic task is parametrised by a time value.  Activity can also be initiated by externally generated interrupts, which may arise from some user action or from the hardware itself. To accommodate this we introduce the triggered tasktype. The last type of activity that we consider is the one-shot task; where some activity is performed and not repeated. To facilitate this we add the oneshot tasktype.  In some cases it may be useful to delay a task for a period of time; we introduce a delay to the TaskBody to facilitate this.
+
=== Goal ===
It may be decided that, during a program’s execution, some of the activities should take precedence over some others.  We introduce priority which allows a developer to assign a numerical value indicating the precedence for scheduling. We adopt the convention that higher priority activities have a greater value, and this corresponds to the Ada convention.
 
  
=Methodological Support=
+
As explained in the design decision part, goal is checked. If it matches the description here above <math>\left(x\in S\right)</math> then ''x'' is stored in an attribute. Moreover, from the set ''S'', we compute every pair ''expression'' & ''position'' equivalent to it. For example, from the set <math>dom(ran(ran(g)))</math>, the map will be computed :
As previously outlined, the atomic steps of a sequential task will be syntactically explicit.  This is in order to facilitate a direct mapping of task steps with events of an abstract machine.   The development approach that we plan to support fits with the general refinement approach of Event-B in that explicit tasking will be introduced as part of a refinement step.  A common approach to specifying a problem is to represent some desired outcome as a single abstract atomic event. Common patterns of refinement of such abstract events found in existing Event-B developments are as follows:
+
*<math>dom(ran(ran(g)))\;\mapsto\;[\;]</math>
 +
*<math>ran(ran(g))\;\mapsto\;[0]</math>
 +
*<math>ran(g)\;\mapsto\;[1,~0]</math>
 +
*<math>g\;\mapsto\;[1,~1,~0]</math>
 +
Only ''range'', ''domain'' and ''converse'' can be taken into account to get all the possibles goals.
  
#Choice refinement:  Event E is refined to E1 [] E2 []…[] En, where each Ei refines E
+
A pair (expression ; position) is said equal to the goal if and only if there exists a pair equivalent to the goal (GoalExp ; GoalPos) and a pair equivalent to the given pair (Exp ; Pos) such as ''Pos = GoalPos'' and ''Exp'' is contained in ''GoalExp''.
#Sequential refinement:  Event E is refined to E1 ; E2 ; … En, where some Ei refines E and the other Ej refine skip.
 
#Loop refinement: Event E is refined to E1 ; do E2 od ; E3, where E3 refines E and E1 and E2 refine skip.
 
  
These patterns motivate a simpler subset of the tasking language as follows
+
=== Hypotheses ===
{| border="0"
 
| TaskBody :=  
 
|-
 
|
 
| Event
 
|-
 
|
 
|  <math>|</math> TaskBody  ;  TaskBody
 
|-
 
|
 
|  <math>|</math> '''if'''    Event  [] … []  Event  '''fi'''
 
|-
 
|
 
|  <math>|</math> '''do'''  Event  '''endwith'''  Event  '''od'''
 
|}
 
  
Initially we will support refinement to this subset by providing special structure-introduction refinement rules in the manner of the refinement calculus.  We will also develop support for a generalisation of this set of rules in which the abstract model consists of a group of atomic events, with each event representing a different possible outcome.  An example use of such a group would be to have an event to represent the normal behaviour of some system feature and a separate event to represent the error behaviour of the feature.
+
As explained in the design decision part, there are two kinds of hypotheses which are recovered. But when hypotheses related to the left member of the goal <math>\left(x\in S\right)</math> are stored, the position of ''x'' is also record. Then, if there is an hypothesis such as <math>\left\{\cdots\;,\;y\mapsto x\mapsto z\;,\;m\mapsto x\;,\;\cdots\right\} = A</math>, then this hypothesis is mapped to the positions <math>\left\{\left[0,~1\right],~\left[1\right]\right\}</math>.
  
The above rules prevent the immediate introduction of nested tasking structures such as nested loops.  Following the approach found in the refinement calculus and common practice in Event-B refinements, such nested structures may be introduced through further refinement steps.  For example, to introduce a nested loop, the outer loop is first introduced and the inner loop is introduced in a subsequent refinement step.  We  will explore generalising the refinement support for tasks to support nesting through refinement along these lines.
+
=== Find a path ===
  
=Timescales=
+
Let's considered the sequent with the following goal : <math>x\in V</math>.
We refer to the tasking language outlined above as Version V1. Our planned timescales for further work on code generation are as follows:
+
We start with the hypotheses which have a connection with the goal's member. Such a hypothesis gives two informations : the position <math>pos</math> and the set <math>S</math> as explained in [[#Hypotheses|hypotheses]]. Then, for each equivalent pair to these one <math>\left(S', pos'\right)</math>, we compute set containing <math>S'</math> ([[#Design Decision#Tactic#Find a path| Find a path 2.]]). For every new pair, we test if it is contained in the goal.
*June 2010: demonstrator tool for language V1.
+
 
*June 2010: initial support for user defined datatypes (mathematical extensions).
+
To be continued.
*From June to October 2010:  experimentation with and assessment of the demonstrator tool on the WP1 and WP3 pilots leading to feedback on V1 and the tool.
+
 
*Jan 2011:  algorithmic language definition V2.
+
= Untreated cases =
*June 2011: prototype tool for V2.
+
 
*From June to October 2011: experimentation with and assessment of the V2 tool on the WP1 and WP3 pilots.
+
Some cases are not treated. Further enhancement may be provided for some.
 +
*<math>x\in A\cup B,\quad A\cup B\cup C\subseteq D\quad\vdash\quad x\in D</math>
 +
*<math>x\in f,\quad f\in A\;op\;B\quad\vdash\quad x\in A\cprod B</math>
 +
*<math>f\ovl \left\{x\mapsto y\right\}\subseteq A\cprod B\quad\vdash\quad x\in A</math>
 +
*<math>x\in f\otimes g,\quad f\subseteq A\cprod B,\quad g\subseteq C\cprod D\quad\vdash\quad x\in (A\cprod C)\cprod(B\cprod D)</math>
 +
*<math>x\in f\otimes g,\quad f\subseteq h\quad\vdash\quad x\in h\otimes g</math>
 +
*<math>x\in \left\{a,~b,~c\right\},\quad\left\{a,~b,~c,~d,~e,~f\right\}\subseteq D\quad\vdash\quad x\in D</math>
 +
*<math>x\in A\cprod B,\quad A\subseteq C\quad\vdash\quad x\in C\cprod B</math>
 +
*<math>x\in dom(f)\cap A\quad\vdash\quad x\in dom(A\domres f)</math>
 +
*<math>x\in ran(f)\cap A\quad\vdash\quad x\in ran(f\ranres A)</math>
 +
*<math>x\in \quad\vdash\quad</math>
 +
*<math>\quad\vdash\quad</math>
 +
*<math>\quad\vdash\quad</math>
 +
*<math>\quad\vdash\quad</math>
 +
*:<math>\bigl(</math> where <math>op_1</math> and <math>op_2</math> are ones of :<math>\quad\rel, \trel, \srel, \strel, \pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij\bigr)</math>
 +
 
 +
[[Category:Design proposal]]

Revision as of 13:28, 9 August 2011

Objective

This page describes the design of the reasoner MembershipGoal and its associated tactic MembershipGoalTac.
This reasoner discharges sequent whose goal denotes a membership which can be inferred from hypotheses. Here an basic example of what it discharges :
H,\quad x\in S,\quad S\subset T,\quad T\subseteq U \quad\vdash x\in U

Analysis

Such sequent are proved by PP and ML. But, these provers have both drawbacks :

  • All the visible are added as needed hypotheses, which is most of the time not the case.
  • They take quite consequent time to prove it (even with the basic example given here above, the difference in time execution is noticeable).
  • If there are too many hypotheses, or if the expression of the x is too complicated, they may not prove it.

This is particularly true when in the list of inclusion expressions of each side of the relation are not equal. For example : H,\quad a\in S,\quad S\subset T_1\cap T_2,\quad T_1\cup T_3\subseteq  U\quad\vdash a\in U

Such a reasoner contributes to prove more Proof Obligations automatically, faster and with fewer needed hypotheses which makes proof rule more legible and proof replay less sensitive to modifications.

Design Decision

Tactic

This part explains how the tactic (MembershipGoalTac) associated to the reasoner MembershipGoal is working.

Goal

The tactic (as the reasoner) should works only on goals such as :

  • \cdots~\in~\cdots

For examples :

  • f(x)\in g\otimes h
  • x\in A\cprod\left(B\cup C\right)
  • x\mapsto y\in A\cprod B

In the latter case, the reasoner won't try to prove that x belongs to A and y belongs to B, but that the mapplet belong to the Cartesian product.

Hypotheses

Now we have to find hypotheses leading to discharge the sequent. To do so, the tactic recovers two kinds of hypotheses :

  1. the ones related to the left member of the goal \left( x\in S\right) (this is the start point):
    • x\in \cdots
    • \cdots\mapsto x\mapsto\cdots\in\cdots
    • \left\{\cdots, x,\cdots\right\}=\cdots
    • \left\{\cdots, \cdots\mapsto x\mapsto\cdots,\cdots\right\}=\cdots
  2. the ones denoting inclusion (all but the ones matching the description of the first point) :
    • \cdots\subset\cdots
    • \cdots\subseteq\cdots
    • \cdots=\cdots

Then, it will search a link between those hypotheses so that the sequent can be discharged.

Find a path

Now that we recovered all the hypotheses that could be useful for the reasoner, it remains to find a path among the hypotheses leading to discharge the sequent. Depending on the relations on each side of the inclusion, we will act differently. f always represent an expression (may be a domain, a range, etc.).

  1. The following sequent is provable because f\subseteq \varphi (f).
    • x\in f,\quad \varphi (f)\subseteq g\quad\vdash\quad x\in g
    • \varphi (f) = f\quad\mid\quad f\cup h \quad\mid\quad h\cup f \quad\mid\quad h\ovl f
  2. The following sequent is provable because \psi (f)\subseteq f.
    • x\in \psi (f),\quad f\subseteq g\quad\vdash\quad x\in g
    • \psi (f) = f\quad\mid\quad f\cap h \quad\mid\quad h\cap f \quad\mid\quad f\setminus h \quad\mid\quad f\ransub A \quad\mid\quad f\ranres A \quad\mid\quad A\domsub f \quad\mid\quad A\domres f
  3. We can generalized the first two points. This is the Russian dolls system. We can easily prove a sequent with multiple inclusions by going from hypothesis to hypothesis.
    • x\in \psi (f),\quad \varphi (f)\subseteq g\quad\vdash\quad x\in g
  4. For some relations, positions are needed to be known to continue to find hypotheses, but it is not always necessary.
    • x\mapsto y\in f,\quad f\subseteq A\cprod B\quad\vdash\quad x\in A
    • x\in dom(f),\quad f\subseteq A\cprod B\quad\vdash\quad x\in A
    • x\in ran(f),\quad f\subseteq A\cprod B\quad\vdash\quad x\in B

By using these inclusion and rewrites, it tries to find a path among the recovered hypotheses. Every one of those should only be used once, avoiding possible infinite loop \left(A\subseteq B,\quad B\subseteq A\right). Among all paths that lead to discharge the sequent, the tactic give the first it finds. Moreover, so that the reasoner does not do the same work as the tactic of writing new hypothesis, it gives all needed hypotheses and added hypotheses in the input.

Reasoner

The way the reasoner must work is still in discussion.

Implementation

This section explain how the tactic has bee implemented.

Positions

As it was said, we may sometimes need the position. It is represented by an array of integer. Here are the possible values the array contains (atomic positions) :

  • kdom : it corresponds to the domain.
    • \left[A\cprod B\right]_{pos\;=\;kdom} = A
    • \left[x\mapsto y\right]_{pos\;=\;kdom} = x
    • \left[g\right]_{pos\;=\;kdom} = dom(g)
  • kran : it corresponds to the domain.
    • \left[A\cprod B\right]_{pos\;=\;kran} = B
    • \left[x\mapsto y\right]_{pos\;=\;kran} = y
    • \left[g\right]_{pos\;=\;kran} = ran(g)
  • leftDProd : it corresponds to the left member of a direct product.
    • \left[f\otimes g\right]_{pos\;=\;leftDProd} = f
    • \left[A\cprod \left(B\cprod C\right)\right]_{pos\;=\;leftDProd} = A\cprod B
  • rightDProd : it corresponds to the right member of a direct product
    • \left[f\otimes g\right]_{pos\;=\;rightDProd} = g
    • \left[A\cprod\left(B\cprod C\right)\right]_{pos\;=\;rightDProd} = A\cprod C
  • leftPProd : it corresponds to the left member of a parallel product
    • \left[f\parallel g\right]_{pos\;=\;leftPProd} = f
    • \left[\left(A\cprod B\right)\cprod\left(C\cprod D\right)\right]_{pos\;=\;leftPProd} = A\cprod C
  • rightPProd : it corresponds to the right member of a parallel product
    • \left[f\parallel g\right]_{pos\;=\;rightPProd} = g
    • \left[\left(A\cprod B\right)\cprod\left(C\cprod D\right)\right]_{pos\;=\;rightPProd} = B\cprod D
  • converse : it corresponds to the child of an inverse
    • \left[f^{-1}\right]_{pos\;=\;converse}=f
    • \left[A\cprod B\right]_{pos\;=\;converse} = B\cprod A

For example, the following expressions at the given positions are equivalent.

\left[f\otimes\left(\left(A\cprod dom(g)\right)\parallel g\right)\right]_{pos\;=\;\left[rightDProd,\;leftPProd,\;kran\right]} = \left[\left(A\cprod dom(g)\right)\parallel g\right]_{pos\;=\;\left[leftPProd,\;kran\right]} = \left[A\cprod dom(g)\right]_{pos\;=\;\left[kran\right]} = \left[dom(g)\right]_{pos\;=\;\left[~\right]} = \left[g\right]_{pos\;=\;\left[kdom\right]}

Some combinations of atomic positions are equivalent. In order to simplify comparison between positions, they are normalized :

  • ran(f^{-1}) = dom(f)\quad\limp\quad \left[f\right]_{pos \;=\; \left[converse,~kran\right]} = \left[f\right]_{pos\;=\;\left[kdom\right]}
  • dom(f^{-1}) = ran(f)\quad\limp\quad \left[f\right]_{pos \;=\; \left[converse,~kdom\right]} = \left[f\right]_{pos\;=\;\left[kran\right]}
  • \left(f^{-1}\right)^{-1} = f\quad\limp\quad \left[f\right]_{pos \;=\; \left[converse,~converse\right]} = \left[f\right]_{pos\;=\;\left[~\right]}

Goal

As explained in the design decision part, goal is checked. If it matches the description here above \left(x\in S\right) then x is stored in an attribute. Moreover, from the set S, we compute every pair expression & position equivalent to it. For example, from the set dom(ran(ran(g))), the map will be computed :

  • dom(ran(ran(g)))\;\mapsto\;[\;]
  • ran(ran(g))\;\mapsto\;[0]
  • ran(g)\;\mapsto\;[1,~0]
  • g\;\mapsto\;[1,~1,~0]

Only range, domain and converse can be taken into account to get all the possibles goals.

A pair (expression ; position) is said equal to the goal if and only if there exists a pair equivalent to the goal (GoalExp ; GoalPos) and a pair equivalent to the given pair (Exp ; Pos) such as Pos = GoalPos and Exp is contained in GoalExp.

Hypotheses

As explained in the design decision part, there are two kinds of hypotheses which are recovered. But when hypotheses related to the left member of the goal \left(x\in S\right) are stored, the position of x is also record. Then, if there is an hypothesis such as \left\{\cdots\;,\;y\mapsto x\mapsto z\;,\;m\mapsto x\;,\;\cdots\right\} = A, then this hypothesis is mapped to the positions \left\{\left[0,~1\right],~\left[1\right]\right\}.

Find a path

Let's considered the sequent with the following goal : x\in V. We start with the hypotheses which have a connection with the goal's member. Such a hypothesis gives two informations : the position pos and the set S as explained in hypotheses. Then, for each equivalent pair to these one \left(S', pos'\right), we compute set containing S' ( Find a path 2.). For every new pair, we test if it is contained in the goal.

To be continued.

Untreated cases

Some cases are not treated. Further enhancement may be provided for some.

  • x\in A\cup B,\quad A\cup B\cup C\subseteq D\quad\vdash\quad x\in D
  • x\in f,\quad f\in A\;op\;B\quad\vdash\quad x\in A\cprod B
  • f\ovl \left\{x\mapsto y\right\}\subseteq A\cprod B\quad\vdash\quad x\in A
  • x\in f\otimes g,\quad f\subseteq A\cprod B,\quad g\subseteq C\cprod D\quad\vdash\quad x\in (A\cprod C)\cprod(B\cprod D)
  • x\in f\otimes g,\quad f\subseteq h\quad\vdash\quad x\in h\otimes g
  • x\in \left\{a,~b,~c\right\},\quad\left\{a,~b,~c,~d,~e,~f\right\}\subseteq D\quad\vdash\quad x\in D
  • x\in A\cprod B,\quad A\subseteq C\quad\vdash\quad x\in C\cprod B
  • x\in dom(f)\cap A\quad\vdash\quad x\in dom(A\domres f)
  • x\in ran(f)\cap A\quad\vdash\quad x\in ran(f\ranres A)
  • x\in \quad\vdash\quad
  • \quad\vdash\quad
  • \quad\vdash\quad
  • \quad\vdash\quad
    \bigl( where op_1 and op_2 are ones of :\quad\rel, \trel, \srel, \strel, \pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij\bigr)