Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Renaming of bound variables with structural lo...

view this post on Zulip Email Gateway (Nov 07 2024 at 16:03):

From: Lukas Bartl <L.Bartl@campus.lmu.de>
Hello,

I've noticed that bound variables are sometimes not renamed even though
they capture free variables after beta-reduction. This happens if the
argument is a structural parameter in the current locale context.

Here is a minimal example, which was tested in Isabelle2023,
Isabelle2024 and with the revision d3c0734059ee of the Isabelle repo:

term "(λy x. x # y) x" (* gives "λxa. xa # x" *)

locale loc =
fixes x :: "'a list" (structure)
begin

term "(λy x. x # y) x" (* gives "λx. x # x" *)

end

Thank you in advance,
Lukas

OpenPGP_signature.asc

view this post on Zulip Email Gateway (Nov 09 2024 at 13:35):

From: Makarius <makarius@sketis.net>
On 07/11/2024 16:56, Lukas Bartl wrote:

Hello,

I've noticed that bound variables are sometimes not renamed even though they
capture free variables after beta-reduction. This happens if the argument is a
structural parameter in the current locale context.

Here is a minimal example, which was tested in Isabelle2023, Isabelle2024 and
with the revision d3c0734059ee of the Isabelle repo:

term "(λy x. x # y) x" (* gives "λxa. xa # x" *)

locale loc =
  fixes x :: "'a list" (structure)
begin

term "(λy x. x # y) x" (* gives "λx. x # x" *)

end

Using the Prover IDE, I see a green x and a blue x in the second example, with
correct markup displayed on C-mouse-hover. So this is fine so far.

I agree that it would be nicer, if printed terms could be read again, and
produced exactly the same result. We never had this claim of "inner-syntax
roundtrip" in the past decades, although some tools hope that it would be
otherwise.

Do you have a concrete application that gets into problems due to this
particular case of inaccurate term printout?

I have recently spent many weeks on refining the inner-syntax engine, and have
come across many fine-points that could be further improved, beyond the
status-quo of well-known limitations. But this is a somewhat open-ended
untertaking: changing assumptions and ambitions after several decades is very
tedious.

Makarius

view this post on Zulip Email Gateway (Nov 10 2024 at 14:13):

From: Lukas Bartl <L.Bartl@campus.lmu.de>
Hi Makarius,

thanks for your answer.

I agree that it would be nicer, if printed terms could be read again,
and produced exactly the same result. We never had this claim of "inner-
syntax roundtrip" in the past decades, although some tools hope that it
would be otherwise.

Do you have a concrete application that gets into problems due to this
particular case of inaccurate term printout?

I am the author of the changeset 81254:d3c0734059ee (variable
instantiation in Sledgehammer and Metis, part of my Master's thesis),
which is a tool that infers the variable instantiations of a Metis proof
and gives the user a suggestion to instantiate the theorems directly
using the "of" attribute. This prints out Isabelle terms and hopes that
they can be read again. I know that this is not guaranteed to work, so
I've done an evaluation to see how often this fails (which is very rare).

Other failures are due to odd/ambiguous syntax, but this particular case
seemed strange to me. Why does it make a difference whether x is a
structural parameter? The bound variables are renamed when x is unbound,
bound in a proof, or without the "(structure)".

Thank you in advance,
Lukas

OpenPGP_signature.asc

view this post on Zulip Email Gateway (Dec 11 2024 at 10:54):

From: Makarius <makarius@sketis.net>
On 07/11/2024 16:56, Lukas Bartl wrote:

Hello,

I've noticed that bound variables are sometimes not renamed even though they
capture free variables after beta-reduction. This happens if the argument is a
structural parameter in the current locale context.

Here is a minimal example, which was tested in Isabelle2023, Isabelle2024 and
with the revision d3c0734059ee of the Isabelle repo:

term "(λy x. x # y) x" (* gives "λxa. xa # x" *)

locale loc =
  fixes x :: "'a list" (structure)
begin

term "(λy x. x # y) x" (* gives "λx. x # x" *)

end

I have made some refinements on inner-syntax printing for the coming
Isabelle2025 release, see also
https://isabelle-dev.sketis.net/rISABELLE7a1001f4c60

* Inner syntax --- the term language *

Note that there is still no ambition to support a full round-trip, meaning
that printed terms can be read again -- and produce exactly the same result.

Makarius

Ex.thy

Last updated: Jan 04 2025 at 20:18 UTC