I know that there have been a lot of other papers on higher-order unification
expressed as an inference system. Maybe Dale Miller knows more about this work.
Larry
On 30 May 2013, at 13:04, Tobias Nipkow nip...@in.tum.de wrote:
Am 30/05/2013 13:49, schrieb Tobias Nipkow:
Am 30/05/2013
Am 30/05/2013 15:11, schrieb Lawrence Paulson:
I know that there have been a lot of other papers on higher-order unification
expressed as an inference system. Maybe Dale Miller knows more about this
work.
I do follow that literature and haven't seen anything relevant on pattern
unification.
On 28 May 2013, at 19:52, Makarius makar...@sketis.net wrote:
... you do type unification of Free/Const/Bound incrementally as you go. So
some ?x::'?a could become a function indirectly, e.g. by unifying c::'?a with
c::nat=bool elsewhere.
This is never done, as far as I know. It is known
On Tue, 28 May 2013, Makarius wrote:
* No change to unify.ML (and especially pattern.ML, which was not really
covered so far). My 3b9c31867707 is backed-out.
* Instead Thm.bicompose_aux in the non-lifted case (i.e. the compose
variants) ensures that the types of all Vars are unified
On Wed, 29 May 2013, Makarius wrote:
Without the latter, src/HOL/Metis_Examples/Clausification.thy crashes at
the very end, due to divergence of types of certain Vars, types that
cannot be unified. This is very odd, but should not be a problem at the
moment: Metis should work as before.
this incident has again reminded me that in the absence of formal proofs about
the code, assertions in the code would be a big step forward. they could have
told us a long time ago that some precondition expected by the unification code
is not guaranteed. lukas and a student had even put together
On 05/27/2013 07:54 PM, Makarius wrote:
Here is another example for Isabelle/Pure, without schematic variables with
different types. It may be be tried before/after my change 3b9c31867707 from
today:
[...]
ML {*
val read = Syntax.read_term (Proof_Context.set_mode
On Tue, 28 May 2013, Christian Sternagel wrote:
Hopefully it is all a bit more precise now. Maybe someone wants to
formalize pattern.ML + unify.ML after 20 years, to pin down the
remaining uncertaincies about type instantiation within these
non-trivial algorithms.
Just for the record, I
On Tue, 28 May 2013, Stefan Berghofer wrote:
Types as well as terms are unified. The outermost functions assume
the terms to be unified already have the same type. In resolution,
this is assured because both have type prop.
So it is the expected behaviour that the unification functions
On Tue, 28 May 2013, Lawrence Paulson wrote:
Historical note: when the original high-order unification code was
written, there was no user-level polymorphism. If my memory is correct,
the TVar constructor did not even exist.
This fits to my speculations when reading the code, and I've tried
On Tue, 28 May 2013, Tobias Nipkow wrote:
According to my understanding, the disunity of types came recursively from the
pattern/unify implementation itself. My guess is that certain schematic
variables first started as ?x::?'a and then diverged with more concrete type
here, and the original
On Tue, 28 May 2013, Makarius wrote:
The crash happens in Thm.bicompose_no_flatten (via Goal.retrofit, which
is the basis of SELECT_GOAL).
This also touches the still open thread on SELECT_GOAL here
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-March/msg00118.html
although
I don't quite understand your commentary, because the result of body_type can
never be a function.
In general, polymorphism in higher-order unification never instantiates a type
variable to a function type, for the reason you seem to hint at: because you
wouldn't know when to stop. This is a
On Tue, 28 May 2013, Lawrence Paulson wrote:
I don't quite understand your commentary, because the result of
body_type can never be a function.
In general, polymorphism in higher-order unification never instantiates
a type variable to a function type, for the reason you seem to hint at:
the disagreement pairs should be fully eta-expanded by this point, though I
haven't looked at the code recently. That would imply that the body_type cannot
be a function type.
Larry
On 28 May 2013, at 16:11, Makarius makar...@sketis.net wrote:
On Tue, 28 May 2013, Lawrence Paulson wrote:
On Tue, 28 May 2013, Lawrence Paulson wrote:
the disagreement pairs should be fully eta-expanded by this point,
though I haven't looked at the code recently. That would imply that the
body_type cannot be a function type.
Can you look now? Notably in Isabelle/3b9c31867707, and the parent of
On Tue, 28 May 2013, Stefan Berghofer wrote:
On 05/28/2013 02:32 PM, Makarius wrote:
The crash happens in Thm.bicompose_no_flatten (via Goal.retrofit, which is
the basis of SELECT_GOAL).
This explains why there is no extra incrementing of Vars, unlike the normal
resolution-family of
On Tue, 28 May 2013, Lawrence Paulson wrote:
the disagreement pairs should be fully eta-expanded by this point
I've spent further thoughts on that: somehow it increases my uneasyness,
since it looks like the full type information needs to be known at some
point to make eta-expansion work,
Am 28/05/2013 13:34, schrieb Lawrence Paulson:
Historical note: when the original high-order unification code was written,
there was no user-level polymorphism. If my memory is correct, the TVar
constructor did not even exist. Polymorphism was only used for type inference
in terms.
Am 28/05/2013 20:52, schrieb Makarius:
On Tue, 28 May 2013, Lawrence Paulson wrote:
the disagreement pairs should be fully eta-expanded by this point
I've spent further thoughts on that: somehow it increases my uneasyness, since
it looks like the full type information needs to be known at
On Tue, 28 May 2013, Tobias Nipkow wrote:
Am 28/05/2013 13:34, schrieb Lawrence Paulson:
Historical note: when the original high-order unification code was written,
there was no user-level polymorphism. If my memory is correct, the TVar
constructor did not even exist. Polymorphism was only
On Tue, 28 May 2013, Tobias Nipkow wrote:
What is a bit unstisfactory here is that it merely avoids certain
crashes of SELECT_GOAL (and maybe other crashes), but the example from
this thread would still not quite work, since the unification problem
is presumably too difficult.
i thought the
Am 28/05/2013 23:53, schrieb Makarius:
On Tue, 28 May 2013, Tobias Nipkow wrote:
Am 28/05/2013 13:34, schrieb Lawrence Paulson:
Historical note: when the original high-order unification code was written,
there was no user-level polymorphism. If my memory is correct, the TVar
constructor did
Hopefully it is all a bit more precise now. Maybe someone wants to
formalize pattern.ML + unify.ML after 20 years, to pin down the
remaining uncertaincies about type instantiation within these
non-trivial algorithms.
Just for the record, I would be interested in joining such an endeavor.
Am 27/05/2013 18:13, schrieb Makarius:
On Mon, 27 May 2013, Stefan Berghofer wrote:
As I pointed out in my previous mail, it is an error to supply disagreement
pairs to unify containing Vars that have the same name but different types.
So
I don't think one should change pattern.ML and
On 04/12/2013 02:18 PM, Makarius wrote:
Just for completeness, I am posting here a self-contained example to expose the
problem.
It looks like I need to discuss it further with Stefan Berghofer, because he
made some reforms there in 2005 that now seem to crash on us.
Hi Markus,
it is not
On Wed, 10 Apr 2013, Makarius wrote:
On Wed, 10 Apr 2013, Johannes Hölzl wrote:
Unfortunately, as you mentioned the excpetion_trace output is not very
helpful, all I see is Seq.make / .copy / .append. The inner functions which
call Envir.var_clash is not shown.
It is relatively easy to
Am Freitag, den 05.04.2013, 14:16 +0200 schrieb Makarius:
On Fri, 5 Apr 2013, Johannes Hölzl wrote:
It looks like the problem is somewhere in the call to
Classical.inst0_step_tac in nodup_depth_tac (clasimp.ML):
clasimp.ML
fun nodup_depth_tac ctxt m i st =
On Wed, 10 Apr 2013, Johannes Hölzl wrote:
Unfortunately, as you mentioned the excpetion_trace output is not very
helpful, all I see is Seq.make / .copy / .append. The inner functions
which call Envir.var_clash is not shown.
It is relatively easy to instrument the main Seq.make abstraction
Hi,
In Isabelle2013 as well as the current development revision (#0a7b4e0384d0)
the following call to auto raises a TYPE exception in envir.ML
8
theory Scratch
imports Main
begin
class test =
fixes P :: 'a set ⇒ bool
lemma
shows P_UNIV [intro]: P UNIV
and P_Int [intro]: P S
On Fri, 5 Apr 2013, Johannes Hölzl wrote:
It looks like the problem is somewhere in the call to
Classical.inst0_step_tac in nodup_depth_tac (clasimp.ML):
clasimp.ML
fun nodup_depth_tac ctxt m i st =
SELECT_GOAL
(Classical.safe_steps_tac ctxt 1 THEN_ELSE
(DEPTH_SOLVE
31 matches
Mail list logo
