Email Gateway (Feb 22 2021 at 12:03): Email Gateway (Feb 22 2021 at 12:03):From: Manuel Eberl <eberlm@in.tum.de>
Prompted by a question from a student of mine, I am wondering why free
argument variables on the left-hand side of a function definition with
"define" have to be fixed manually with "for" for it to work:
define a :: "nat ⇒ nat" where "a x = 2 * x"
When writing it like this, the "x" is not fixed and therefore the
"definition" does not work. When you add a "for x", it seems to work.
Is there a reason for this behaviour? Would it be possible to fix such
variables automatically, mirroring the behaviour of e.g. the
"definition" command?
Manuel
smime.p7s
Email Gateway (Feb 22 2021 at 12:23):From: Makarius <makarius@sketis.net>
Such "auto fixes" only work for toplevel specification commands, and that is
already quite delicate and sometimes fragile.
Within the Isar proof languages with its arbitrary nesting of scopes, local
parameters need to be properly fixed. Note that the above "x" could be a
"constant" from an outer scope.
Further note that our ultra-flexible term syntax makes it impossible to say
e.g. that "a" wants to bind its argument (in contrast to ML: "fun a x = ...").
Much more could be said about the overall language design and resulting
decisions. In retrospect over more than 20-25 years, I would be now slightly
more explicit in the scopes: implicit variable declarations are often
confusing, both for the system and the human using it. (The more recent 'for'
context for various language elements make things more robust and flexible.)
Makarius
Email Gateway (Feb 22 2021 at 12:23):From: Makarius <makarius@sketis.net>
Such "auto fixes" only work for toplevel specification commands, and that is
already quite delicate and sometimes fragile.
Within the Isar proof languages with its arbitrary nesting of scopes, local
parameters need to be properly fixed. Note that the above "x" could be a
"constant" from an outer scope.
Further note that our ultra-flexible term syntax makes it impossible to say
e.g. that "a" wants to bind its argument (in contrast to ML: "fun a x = ...").
Much more could be said about the overall language design and resulting
decisions. In retrospect over more than 20-25 years, I would be now slightly
more explicit in the scopes: implicit variable declarations are often
confusing, both for the system and the human using it. (The more recent 'for'
context for various language elements make things more robust and flexible.)
Makarius
Email Gateway (Feb 22 2021 at 12:27):From: Jakub Kądziołka <kuba@kadziolka.net>
I agree that changing the behavior could be infeasible. However, perhaps
it would be enough to emit a warning message when one uses 'define'
without 'for'?
Regards,
Jakub Kądziołka
Email Gateway (Feb 22 2021 at 12:29):From: Makarius <makarius@sketis.net>
Warnings are generally bad design: the system needs to be strict about its
syntax and emit proper errors.
Within the Prover IDE, such errors could contain completion information to
help the user get the input right, but that is quite some extra work and not
always done.
Makarius
Email Gateway (Feb 22 2021 at 13:29):From: Manuel Eberl <eberlm@in.tum.de>
Is there any context in which define f where "f x y = …" makes any
sense without a "for x y" afterwards?
Manuel
smime.p7s
Email Gateway (Feb 22 2021 at 14:26):From: Makarius <makarius@sketis.net>
E.g. when x y are absent.
(Are you proposing special cases to complicate things?)
Makarius
Email Gateway (Feb 22 2021 at 14:39):From: Makarius <makarius@sketis.net>
Maybe part of the confusion is from mistaking Isabelle/HOL as a functional
programming language, where definitions have a special syntactic status. In
contrast Isabelle definitions are logical specifications based on equations.
(Definitions like 'inductive' are again more general in this respect.)
Here is a fun-fact that may help to see the difference more clearly. The
successor function defined in ML, Haskell, Scala:
fun a a = a + 1;
a :: Int -> Int
a a = a + 1
def a(a: Int): Int = a + 1
The lambda-term language of the Isabelle logical framework works quite
differently, it cannot (and should) not imitate that.
Makarius
Last updated: Jul 15 2022 at 23:21 UTC