82cb380
committed
Commits
Comments (0)
Files changed (1)

+43 16doc/final/index.tex
doc/final/index.tex
The nice thing about not having to care about any leftover formulas (as it is simply a failure when that happens)
is that no explicit sequentialization is needed in cases when two subproofs have to be found. The MonadPlus abstraction along
with operators from the Control.Applicative module can shine here. We can also write the whole proof search as
+is that no explicit sequentialization is needed in cases when two subproofs have to be found. The \verbMonadPlus abstraction along
+with operators from the \verbControl.Applicative module can shine here. We can also write the whole proof search as
As an illustration we present the procedure for performing inversion on the right from the full focusing prover
We have implemented basic version of lazy splitting, where judgments are annotated by input ($\Delta_I$)
+We have implemented a basic version of lazy splitting, where judgments are annotated by input ($\Delta_I$)
the proof representation. Each function in prover gets an input resources as a parameter and returns
The NaiveLS prover is developed from prover without resource management, so it is just a enhanced version.
+proofs  everything can be handled internally in the proof search algorithm. Each function in then prover receives
+the current input resources as a parameter and the output resources are returned along with the proof.
+The NaiveLS prover is developed from the prover without resource management, so it is just an enhanced version.
+First, we note that the version without resource management tries all possible ways to split the linear context...
just passes input and output resources (both provers are written in flavor of continuation passing style).
On the other hand new algorithm need to compute subproofs in sequential way, while in old algorithm
+...while the version with lazy splitting simply passes the input and output resources to be handled in the recursive calls and the final continuation:
+Both provers are written in a flavor of continuation passing style, but the second one has to adhere to a more strict CPS discipline.
+while in the old algorithm these computations are independent (and could even be executed in parallel).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+The results of benchmarking suggest that it would certainly be worth the while to implement the improved resource management
We tried to use modern Haskell features for parallelization \cite{Marlow}, but we did not achieve gratifying result.