Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Variable both free and bound?!


view this post on Zulip 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

view this post on Zulip 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>):

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Sep 25 2021 at 10:20 UTC