Re: [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning



On Fri, 22 Mar 2013, Andreas Lochbihler wrote:

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.

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


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