- some work on extensions:
the alternative definition of lpx_sn and llpx_sn is useless since it is recursive
llor seems to contain a bug in the referred components
- some work pointwise extended reduction:
we restore the "full" version and use it for the normaliztion of extended reduction
we still use "lazy" version for the "big-tree" theorem
commit completed:
- pointwise ordinary reduction:
we park the "lazy" version and we restore the "full" version
annotating the source with our understandings
- pointwise extended reduction:
we use the "lazy" version for now
a better understanding of the relationship between the "full" version
and the "lazy" version (lpx_sn_llpx_sn) allows to link the two
Ferruccio Guidi [Tue, 25 Mar 2014 19:55:08 +0000 (19:55 +0000)]
- partial commit: just the components below "computation"
the development of lazy pointwise extensions continues ...
- we parked not-lazy pointwise extensions in etc
Ferruccio Guidi [Sat, 8 Mar 2014 17:32:55 +0000 (17:32 +0000)]
we define the lazy poinwise extension of a relation, that should
allow to derive lleq with corrected lleq_lref, and a new defininition
for lpx (and derivatives), which now contains a bug too :( being not lazy
- we revise the definition of lazy equivakence since lleq_lref contains a bug
Code changed a bit to make it work as before with OCaml 4.0.
Without this patch, the refresh of the textual widget (e.g. the update
of the locked part) is not immediately done.
This is roughly the visual behaviour the user expects. On the other hand,
we also expect the threads that execute and that responsible for the UI
to work in parallel, which is not the case. The code I just touched stops
the worker thread for, on average, 0.1s per tactic, which is really a lot.
Switching to a multiprocess implementation (in place of a multithread) does
not seem easy. Bad OCaml, bad.
Hocus-pocus code to use the old (and deprecated) implementation of
Hashtbl.hash because the new one changes the behaviour of automation,
breaking the library.
Bug fixed: the tactic to analyze the term and understand whose inductive
type it belongs to did not put the sort in whd before concluding that
it was not a sort.
OCaml 4.0 detects a not handled case.
I hope the assertion will never be reached, but I ignore why.
I think this is really a bug and code must be written there.
Ferruccio Guidi [Fri, 21 Feb 2014 16:36:20 +0000 (16:36 +0000)]
- main proposition on lsx finally proved!
- long awaited equivalence for local environments is now set up (coequivalence is in etc in case of need)
- unused results on append parked in etc
- some additions to ynat
Ferruccio Guidi [Wed, 29 Jan 2014 18:55:32 +0000 (18:55 +0000)]
bug fix in the notation of normal forms, now we specify that they are
normal forms for reduction. This will allow to enable normal forms for
substitution ...
Ferruccio Guidi [Sun, 26 Jan 2014 10:08:33 +0000 (10:08 +0000)]
- nat: some additions, plus_minus_commutative renamed plus_minus_associative
- lambda: we study terms in which references are by "level" rather
than by "depth" aiming at establishing a bijection between the two
representations, we start the support for distributed notation as in lambdadelta
Ferruccio Guidi [Sat, 18 Jan 2014 22:05:09 +0000 (22:05 +0000)]
- commit of the "reduction" component with two additions ...
- formal bug fix in extended substitution under a binder: now we
follow the paradigm used for reduction under a binder
Ferruccio Guidi [Sat, 14 Dec 2013 22:18:47 +0000 (22:18 +0000)]
- "big tree" theorem is now proved up to some conjectures involving
just computation
- redefined "big tree" proper computation now replaces its restricted
form and is transitive
- improved definition of "big tree" proper reduction involves lazy
extended computation for local enviroments
Ferruccio Guidi [Sun, 1 Dec 2013 20:57:54 +0000 (20:57 +0000)]
- improved arithmetics for natural numbers with infinity
- some properties of equivalence for local environments
- improved lazy equivalence for local environments
- we commit just the "relocation" component