Email Gateway (Jan 08 2021 at 22:34): Email Gateway (Jan 08 2021 at 22:34):From: Jakub Kądziołka <kuba@kadziolka.net>
Hello,
consider the following theory:
theory Scratch
imports Main
begin
fun inc :: "nat ⇒ nat" where
"inc x = Suc x"
definition inc' :: "nat ⇒ nat" where
"inc' x = Suc x"
end
When you hover over either of the x's in fun inc (with Ctrl held), the
following tooltip appears:
free variable
bound variable
:: nat
Similarily, the tooltip for the x's in definition inc' is:
free variable
:: nat
bound variable
(these observations are equally valid for both Isabelle2020 and
Isabelle2021-RC1)
I find this quite curious, as 'free' and 'bound' seem to be polar
opposites...
Kind regards,
Jakub Kądziołka
Email Gateway (Jan 10 2021 at 16:38):From: Buday Gergely István via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
The set of free and bound variables are not necessarily distinct.
See this example:
(\x.x) (\y.x)
Here x is bound in \x.x because of \x but it is also free in the \y.x part.
Idézet (Jakub Kądziołka <kuba@kadziolka.net>):
Email Gateway (Jan 10 2021 at 16:39):From: Jakub Kądziołka <kuba@kadziolka.net>
I am aware. However, in my example, Isabelle claims that a particular
use of the name x is both free and bound at the same time.
Regards,
Jakub Kądziołka
Email Gateway (Jan 10 2021 at 18:21):From: Makarius <makarius@sketis.net>
On 08/01/2021 23:24, Jakub Kądziołka wrote:
fun inc :: "nat ⇒ nat" where
"inc x = Suc x"When you hover over either of the x's in fun inc (with Ctrl held), the
following tooltip appears:free variable
bound variable
:: nat
As a general principle, the Prover IDE reveals aspects of the formal status of
text processed by the prover. This processing often has several stages, and a
piece of text may get cumulative markup as a trace of the internal stages.
There is considerable complexity in the internals as well as in the external
representation of terms. Over the past decade, I have tried hard to expose
that in the IDE such that it makes somehow sense.
In the concrete situation above, the body of the function definition has
implicitly bound frees: x is fresh in the scope and later closed like this:
fun inc :: "nat ⇒ nat"
where "⋀x. inc x = Suc x"
There are other situations where seemingly free variables are treated like
implicit bounds, e.g. in simplifier traces.
I find this quite curious, as 'free' and 'bound' seem to be polar
opposites...
Just from the wording of it, in mathematics a set can be both "open" and
"closed" (in the sense of topology).
In formal logic, the words "free" vs. "bound" are traditional, but to some
extent also misleading: "bound" actually means the binder is within the term,
or somehow tightly attached to it; "free" means the binder is further outside
or implicit.
Further note that Isabelle/Isar also has light-brown Skolem constants: these
are local variables of a proof context --- technically "free" but morally "bound".
Makarius
Email Gateway (Jan 10 2021 at 18:34):From: Makarius <makarius@sketis.net>
Here is a formally checked version of the example:
theory Scratch
imports Main
begin
term ‹(λx. x, λy. x)›
end
C-hovering in the Prover IDE reveals that the double use of a name "x" is
merely superficial: the variables have different scopes and different
most-general types. These are two independent variables.
Further details can be inspected in Isabelle/ML: ML ‹val t = @{term ‹(λx. x,
λy. x)›}›
It shows that bound "x" is actually just a nameley de-Bruijn index, together
with a comment-field for parsing and printing.
Makarius
Last updated: Jan 04 2025 at 20:18 UTC