Email Gateway (Aug 18 2022 at 20:16): Email Gateway (Aug 18 2022 at 20:16):From: Makarius <makarius@sketis.net>
On Wed, 13 Jun 2012, Steve Wong wrote:
Just a quick question: how come Isabelle keeps a distinction between
free and schematic variables?
Free means "fixed" and schematic "arbitrary". In informal mathematics you
say "let x be arbitrary, but fixed". Which means it is first made a local
free/fixed thing, and in the result it can then be arbitrary.
In the Isar proof language you write down fixed things, and get
potentially arbitrary results from it. The free vs. schematic marker
implements that idea formally in the underlying logical framework.
It seems that free variables in a goal are converted to schematic
anyway, so what are the benefits of keeping them distinct?
When you say "in a goal", you mean the so-called "eigen context" of a
statement, e.g.
theorem fixes x :: 'a shows "x = x" ..
Here 'a and x are fixed, and in the result everything is then schematic,
at least in this example. In general, the context can still keep other
things fixed (say via 'locale' or 'context' or within a nested proof).
In fact, a mixture of fixed and schematic variables characterizes genuine
locality in Isabelle, as opposed to the old scheme from the 1980/1990-ies
where everything was either free or schematic.
Makarius
Email Gateway (Aug 18 2022 at 20:16):From: Makarius <makarius@sketis.net>
Both free and schematic variables belong to Isabelle/Pure, just like bound
variables via !!x or %x. You could argue if Isabelle/HOL has actually
variables on its own -- it just re-uses many things from Pure directly,
including the type system, for example.
Makarius
Email Gateway (Aug 18 2022 at 20:23):From: Steve Wong <s.wong.731@gmail.com>
Hi,
Just a quick question: how come Isabelle keeps a distinction between free
and schematic variables? It seems that free variables in a goal are
converted to schematic anyway, so what are the benefits of keeping them
distinct?
Cheers
Steve
Email Gateway (Aug 18 2022 at 20:23):From: Ramana Kumar <rk436@cam.ac.uk>
How would you propose to fuse the concepts?
Do you mean Isabelle/HOL should use free variables wherever it
currently uses schematic variables, or schematic variables wherever it
currently uses free, or should use something different for both?
Thinking about that question might make it more obvious why there are
two kinds of "free" variable.
(I'm looking forward to an expert's answer, though: as I understand
it, the distinction is fundamentally unavoidable because one kind of
variable is in the object-logic syntax and the other is a meta-logic
variable. But I may be wrong about this.)
Email Gateway (Aug 18 2022 at 20:23):From: Lawrence Paulson <lp15@cam.ac.uk>
The distinction is useful in the course of a proof. Free variables typically represent fixed parameters of the statement being proved. Schematic variables represent unknown quantities such as existential witnesses, where any single value might be supplied. If such a quantity is ?n, a natural number, then replacing ?n by 0 would be appropriate in a proof. However, if the statement being proved involves a natural number n as a parameter, it would not be acceptable to replace n by 0 and prove the much simpler statement resulting from that substitution.
Once the theorem has been proved, making all variables schematic makes it possible to apply the theorem for arbitrary values of n (which will now be ?n).
Larry Paulson
Email Gateway (Aug 19 2022 at 07:48):From: Ramana Kumar <rk436@cam.ac.uk>
Could I summarise the difference between free and schematic variables like
this:
Free variables came from the statement you want to prove, whereas schematic
variables came from other facts that are already known to be true.
(Thus, free variables must be fixed during a proof, they cannot be
instantiated. Because they were never instantiated, they can become
arbitrary after the proof is completed. Schematic variables can be
instantiated at any time, because they came from some proof in which they
were originally treated as fixed.)
Last updated: Apr 23 2024 at 20:15 UTC