Commit 113291fc authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Add comparison for paths.

parent 2a63b4cb
......@@ -31,8 +31,21 @@ operations, their approach works also in the presence of side-effects. Although
the choices made by our and their approach seems diametrically opposed
(the Boolean output of few pure operations vs.\ any output of any
expression), they share some similar techniques. For instance, our
deduction system for $\vdashp$ plays the same role as
...~\citet[Figures 4\&7]{THF10} KIM TO BE COMPLETED
deduction system for $\vdashp$ plays a similar role as
the proof systems and \textsf{update} function of \citet[Figures 4,
7 \& 9]{THF10}. In that framework, when one needs to type a variable
(judgemetn ``$\Gamma \vdash x:\tau$''), one has to be able to prove
that the logical formula $\tau_x$ holds (under the hypotheses of
$\Gamma$). This atomic formula may not be directly available in
$\Gamma$ but may
be proven by a combination of logical deduction rules (Figure~4), or
by recursively exploring a path leading to $x$ (Figure~7 and ~9) a
path being a sequence of \textbf{cdr} or \textbf{car} applications,
much like our $f$ and $s$ components of paths. This idea is also
present in our $\vdashp$ with differences pertaining to our type
framework and design choices : type restrictions can be encoded using
set-theoretic intersections and negations (instead of meta-functions working on the
syntax of types) and our richer language of paths components.
One area where their
work goes further than ours is that the type information also flows
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment