#
0522ac05 |
|
08-Nov-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get reductionEval to compile under mosml. Knock-on change from 2c29276d6 (similar to e78efa92e)
|
#
2c29276d |
|
04-Nov-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
ThmSetData passes thms *and* names to consumers The names were always available, but the API now changes so that consumers get names as well as theorem values. They can ignore the names of course. (In this context, consumers are things like the stateful rewriter, the monotonicity rule database, the TFL congruence rule database etc.) This will be helpful in allowing the stateful simpset to know what its theorems are called, which is progress with Github issue #313 (to allow easy removal of rewrites from a call to the simplifier).
|
#
1bb5dd5f |
|
02-Aug-2012 |
Michael Norrish <michael.norrish@nicta.com.au> |
Adjust (and reduce) interface to ThmSetData. The change is to add an extra string parameter to the callback function that the client provides. This is the name of the theory which has stored the theorems. This change prompted the changes to computeLib, IndDefLib and DefnBase. The reduction was to remove the ThmSetData's new function, forcing BasicProvers to use new_exporter. This was possible because of the extra information provided to its call-back. I also wrote some test-cases mimicking the original problem that Magnus and Ramana had, and prettied the warning output. This closes #73.
|
#
8ccbf259 |
|
25-Mar-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Preliminary thoughts on using relsimp fragments in my lambda-calculus code. The new BETA_ss does the right thing (enables rewriting wrt beta- equivalence), but actually adjusting the existing proofs to use this presentation of the technology seems like undue hard work right now.
|
#
640080d4 |
|
14-Jun-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix another breakage caused by me changing names in chap2Theory.
|
#
47f6c4df |
|
11-Apr-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Export bstore_thm from reductionEval, and use it in a few more places. (This is the function that stores a theorem, and adds it to the stateful lambda-calculus rewriter.)
|
#
e1cbbd7f |
|
14-Mar-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix compilation error caused by change to SSFRAG's filter field.
|
#
2391bc1b |
|
11-Feb-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Provide and use a new loadable-theory-data entry point. This function, new_exporter, makes it even easier to export theorems in a theory segment.
|
#
1ab9ffa2 |
|
03-Feb-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Slightly polish ThmSetData, and start to use it in lambda example.
|
#
1271d3b1 |
|
09-Nov-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Move some theorems around; mainly to put cfindleast into churchnumTheory.
|
#
9b32d943 |
|
29-Sep-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Demonstrate the easy closure properties for recursive sets (empty, UNIV, and finite sets are recursive; they are closed under union, complement and intersection). Make much use of the fact that it is legitimate to rewrite with beta-reduction under the bnf_of function: M == N ==> (bnf_of M = bnf_of N) Adding this to my weakening congruences did break the proof of one of my Halting Problem theorems, but a little abbreviation hackery solved that.
|
#
fcc09cc8 |
|
26-Apr-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Weak-head reduction (like all the others) can't create new free variables. Also add the substitutivity result for w.h. as a congruence rule.
|
#
e4599942 |
|
21-Apr-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More support for weak head reduction, including a simpset for rewriting with it.
|
#
592c6b55 |
|
30-Mar-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Use the new add_relsimp facilities in simpLib to implement the system provided by reductionEval, and to simplify the proofs in chap2Script. While I'm at it, add definitions and characterising theorems about combinators B, C, and Y in chap2Theory.
|
#
d2800ab2 |
|
22-Mar-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Changes so that the weakened rewriting of lambda-terms now happens with respect to beta-equality (==), rather than beta-reduction (-b->*). This gives us access to more rewrites. In particular, we get things like church (SUC n) @@ z @@ f == f @@ (church n @@ z @@ f) which is a nice recursive characterisation of what church numerals do, and saves us from having to do too many ghastly things with FUNPOW. With the above equation, neither side reduces to the other (they have a common reduct of course), and so it wasn't a usable rewrite when using -b->*. In addition, to the above, I set up a natrec combinator, which would get typed : 'a -> (num -> 'a -> 'a) -> num -> 'a if we were in a typed world. This combinator gets access to the value of the recursive argument, making predecessor easier to define. Also, give an equation like the one above for church for the cDB function. Many proofs are shorter. Some are slower, but the shortness of expression won me over.
|
#
aaaa7160 |
|
17-Mar-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix for handling of conditional rewrites for beta-reduction.
|
#
2e2f1a41 |
|
13-Mar-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix reductionEval so that I can have conditional rewriting wrt beta-reduction. I.e., something along the lines of |- P ==> M -b->* N will successfully 'rewrite' M to N after successfully discharging P. Proofs in the computability directory get *considerably* shorter, particular the characterisation of the ceqnat relation.
|
#
fced617a |
|
13-Mar-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Symbolic evaluation for beta and normal order reduction is coming along well. The proofs in bool are much nicer. The churchnumScript.sml is broken until I get implement conditional rewriting in my rewriter for beta-reduction (should be easy). The proofs there should become considerably nicer.
|
#
cfaa2343 |
|
12-Mar-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fully support weaker relations than equality that aren't also constants. Start to implement a reduction engine for beta-reduction in the lambda-calculus. Still some wrinkles to work out.
|