Re: [isabelle] The Incredible Proof Machine



-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

Dear Joachim,

Sorry, I really can't remember the details, but I'm pretty sure that
it was just about the concrete implementation of the "devar" function
(section 6; so it should not be related to section 9).

I hope that Julian will fill in the details at some point ;)

cheers

chris

On 09/25/2015 12:33 PM, Joachim Breitner wrote:
> Dear Christian,
> 
> Am Freitag, den 25.09.2015, 11:13 +0200 schrieb Christian
> Sternagel:
>> 2) Since you mentioned the nice paper by Tobias (on higher-order 
>> pattern unification). Did you also implement the "devar"
>> optimization of the same paper? Just recently, Julian Nagele (a
>> PhD student in our group; who I also CC'ed), stumbled upon a
>> problem with "devar" when implementing the same algorithm. I do
>> not remember the details (maybe Julian could comment), only that
>> a little bit of hg-digging revealed the following changeset:
>> 
>> changeset:   12232:ff75ed08b3fb user:        berghofe date:
>> Mon Nov 19 17:34:02 2001 +0100 summary:     Replaced devar by
>> Envir.head_norm
>> 
>> (referring to src/Pure/pattern.ML)
>> 
>> I'm curios to whether others already had a similar experience
>> with "devar" and what the intention behind this change was?
> 
> Are you referring to âÂ9 Minimizing new variablesâ in the paper?
> Since this seems to be part of the ML code in 
> http://www21.in.tum.de/~nipkow/pubs/lics93-alpha.ML which I based
> my implementation on, I also have that. If there is anything wrong
> with it, Iâd like to know of course!
> 
> Thanks, Joachim
> 
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2

iQIcBAEBCAAGBQJWBTfoAAoJECdPcHF8FDHN9JcQALciOoEOX4B5oATc3kPTqHMU
KkM+0RqJmzgJz74SmqqkEtQjm/ecfGP8CYTl3g8cctHjiJD/V1+IFi7whc8o/75I
gQ77hh6g7UBx+h8Gv4r8RLonBN59A4FKv7iBmzy0T9PsAAL6uhSlGs6Andgmj4oP
90yMKvC/7wa5Ub0YLVS8K8MPgppYCKh+oTi+xIf9nHzKQRKAVLgu5ot/whF9is3C
uniP428jmryLElJlM+LHm87PMmvGxd0XaRG9LpMRa9NxD0r17dOEG1RXNhVdxcjj
ixHKP8R7nTQD6VwBxMwxBgY4NvbLCZWQT7y/Agmitg3CF9zdA89tZKt2EX8Cqlnr
MSg8yjH8oiW3G6/2msAep9hiqXylgtJNqnrgW6DjorFjLkLNXWLmwdz6TT1mHg24
/+Cbf2hHUZJERdK/qZ48TOGVaI66x1Szf5JXOwK4McBjDLtBgBe2lFMh4aFQ6HQF
9XVF0tEG2pC170JBscbSuXioeNdUF+u6ggqP0vDKDOS/I8kzWgdd5FSqCC1BQBth
iLSlTlj8c76BE4Zzu+mb7mWth63qv3RbKU4PQw8cmYSEBDRa4tYWPY1OvO+udSOG
AXsc5+GOw3BBwMFyUS9Agw8PAsv6rJEhv4OXaiYGi8ZyMZu8pRDCMNA2IRosLJxs
YTCvUwAlaMQ0zL4re4DR
=5Wgq
-----END PGP SIGNATURE-----




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.