Email Gateway (Aug 19 2022 at 10:34): Email Gateway (Aug 19 2022 at 10:34):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Cornelius,
you see already in the output of, e.g.,
term "{(v, v). v : {''a'', ''b''}}"
that the non-linear pattern "(v, v)" is "not accepted" (or rather
implicitly translated into a linear one).
Currently, for set-comprehension, a syntax translation is specified (in
Set.thy), which is conceptually very simple and reuses the "pttrn" token
category. "pttrn" is initially equivalent to plain identifiers and only
later extended, e.g., in Product_Type.thy to allow pairs.
It might be possible to incorporate error messages in the setup in
Product_Type.thy. But as you will see there, even the current "simple"
setup is rather involved.
cheers
chris
Email Gateway (Aug 19 2022 at 10:34):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Cornelius,
You want "{(v, v) | v. v : {''a'', ''b''}}". The syntax for set
comprehension is such that you should explicitly mention bound variables
between "|" and ".", i.e., v in this case. In some simple cases, this
can be avoided, and you ran into one of them:
"{(x, y). P}" is pretty syntax for
"Collect (prod_case (%x y. P))", so in your case, you get
"Collect (prod_case (%v v. v : {''a'', ''b''}))"
See how the second v in %v v. ... hides the former.
There is no warning because it is perfectly normal to rebind a variable
name in a lambda abstraction.
Best,
Andreas
Email Gateway (Aug 19 2022 at 10:34):From: Tobias Nipkow <nipkow@in.tum.de>
Am 22/03/2013 08:15, schrieb C. Diekmann:
Hi,
I found a very counterintuitive problem with tuples in set notation.
I want to define some sort of reflexive closure.
When I write {(v, v). v ∈ {''a'', ''b''}} I hope to get {(''a'',
''a''), (''b'', ''b'')}. However, I found that
lemma "(''a'', ''b'') ∈ {(v, v). v ∈ {''a'', ''b''}}" by(simp)
and even
lemma "(''xyz'', ''b'') ∈ {(v, v). v ∈ {''a'', ''b''}}" by(simp)With
declare[[show_types]], I traced the problem and found:
lemma "{(v, v). v ∈ {''a'', ''b''}} = {(x, y). y∈{''a'', ''b''}}" by simp
My set is actually translated into {(va∷'a, v∷char list). v ∈ {''a'', ''b''}}
As Christian already said, this is the explanation. Just like in functional
programming, patterns must be linear. Unlike in FP, Isabelle silently translates
your non-linear pattern into a linear one (for set comprehensions only). It
should of course be rejected but at the time I was too lazy to implement this
(it would have meant going to the ML level). Of course these days the philosophy
is still to accept it but use the right interface to warn the user that what he
typed is not what he got and he better beware ;-)
Tobias
Why does this happen?
Why wasn't there even some warning that a new variablevawas introduced?Regards
Cornelius
Email Gateway (Aug 19 2022 at 10:36):From: Makarius <makarius@sketis.net>
I agree that it is perfectly normal, just like term "λx x x. x", and no
warning or error is to be expected.
In Scala there is occasionally an error with situations that look similar
to an HOL or ML person, but are actually more complex due to slightly
different scoping rules for that JVM-derived language. So it leads to
very counterintuitive errors for me occasionally.
Another counter-example is Isabelle/HOL list-comprehension, which has an
entry in the "Confusing Isabelle error messages" category here:
https://isabelle.in.tum.de/community/Error_Messages#Misleading_variable_naming_in_list_comprehension
Every time I pass by there, I wonder if it is still up-to-date, and if
there is a way to make the syntax more conformant to Isabelle lambda
calculus scoping rules --- or if there are more fundamental problems
behind that. (IIRC, Christian Sternagel was the last one asking that some
months ago, but without any conclusion so far.)
Makarius
Last updated: Nov 21 2024 at 12:39 UTC