Email Gateway (Aug 22 2022 at 17:42): Email Gateway (Aug 22 2022 at 17:42):From: Makarius <makarius@sketis.net>
So what is the reasoning behind it?
I still have adhoc_overloading on my list of things to be integrated
properly into Pure, such that it works together with abbreviations. It
is one of the things to happen really soon (i.e. within 1 week, 1 month,
1 year, 1 decade).
Makarius
Email Gateway (Aug 22 2022 at 17:42):From: Makarius <makarius@sketis.net>
I see this complexity -- inherited from distant past -- as a motivation
to do away with overloading of funpow/compow. Instead it could be either
done with abstract syntax (adhoc_overloading) or concrete syntax (notation).
(It is something to be reconsidered shortly after the Isabelle2018 release.)
Makarius
Email Gateway (Aug 22 2022 at 17:42):From: Lars Hupel <hupel@in.tum.de>
So what is the reasoning behind it?
Generally being conservative about what gets included by default.
According to Florian, there are still some strange effects there. Of
course, they could be ironed out. The judgment on adhoc_overloading was
based on the current state, not on a future state.
Email Gateway (Aug 22 2022 at 17:47):From: Peter Lammich <lammich@in.tum.de>
Hi List.
Consider the following definition
definition "test f n a ≡ (f^^n) a"
Isabelle answers with a strange error message here:
(*
Malformed dependency of test('a, 'b) -> compow('a ⇒ 'b)
(restriction compow('a ⇒ 'a ⇒ bool) from
"Transitive_Closure.relpowp_def")
The error(s) above occurred in definition "test_def_raw":
"test ≡ λf n. compow n f"
*)
What happened here? How to read this error message? Note that the term
term "test f n a ≡ (f^^n) a"
is well-typed, and Isabelle infers f::'a=>'b
Workaround: Explicitly constrain the type of f:
definition test :: "('a ⇒ 'a) ⇒ _" where "test f n a ≡ (f^^n) a"
Works.
Email Gateway (Aug 22 2022 at 17:47):From: Nemouchi Yakoub <y.nemouchi@gmail.com>
Hi Peter,
For some reason you have an extra variable a.
For some reason (f^^n) is of type ::'a it takes no argument.
Cheers,
Yakoub.
2018-07-09 7:57 GMT-04:00 Peter Lammich <lammich@in.tum.de>:
Email Gateway (Aug 22 2022 at 17:47):From: Nemouchi Yakoub <y.nemouchi@gmail.com>
Hi,
However you are right I am puzzled by the pattern of the definition which
is:
consts compow :: "nat ⇒ 'a ⇒ 'a"
abbreviation compower :: "'a ⇒ nat ⇒ 'a" (infixr "^^" 80)
where "f ^^ n ≡ compow n f"
Hope that no one had fun by defining syntactic sugar for consts compow ::
"nat ⇒ 'a ⇒ 'a"
Best wishes,
Yakoub.
2018-07-09 8:58 GMT-04:00 Nemouchi Yakoub <y.nemouchi@gmail.com>:
Email Gateway (Aug 22 2022 at 17:47):From: Lars Hupel <hupel@in.tum.de>
However you are right I am puzzled by the pattern of the definition which
is:
This is regular overloading in Isabelle, and in that instance, its use
is indeed a bit puzzling.
Is there a compelling reason why "compow" is not an ad-hoc overloaded
constant?
Cheers
Lars
Email Gateway (Aug 22 2022 at 17:47):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
This is regular overloading in Isabelle, and in that instance, its use> is indeed a bit puzzling.> > Is there a compelling reason why "compow"
is not an ad-hoc overloaded> constant?
well, referring to Isabelle2018-RC0, compow is and ad-hoc overloaded
constants:
(in Nat.thy)
consts compow :: "nat ⇒ 'a ⇒ 'a"
with instances
(in Nat.thy)
overloading
funpow ≡ "compow :: nat ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)"
begin
primrec funpow :: "nat ⇒ ('a ⇒ 'a) ⇒ 'a ⇒ 'a"
where
"funpow 0 f = id"
| "funpow (Suc n) f = f ∘ funpow n f"
end
(in Transitive_Closure.thy)
overloading
relpow ≡ "compow :: nat ⇒ ('a × 'a) set ⇒ ('a × 'a) set"
relpowp ≡ "compow :: nat ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool)"
begin
primrec relpow :: "nat ⇒ ('a × 'a) set ⇒ ('a × 'a) set"
where
"relpow 0 R = Id"
| "relpow (Suc n) R = (R ^^ n) O R"
primrec relpowp :: "nat ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool)"
where
"relpowp 0 R = HOL.eq"
| "relpowp (Suc n) R = (R ^^ n) OO R"
end
The key idea behind that all once indeed was to have shared ^^ syntax
for operations alluding to different kinds of composition, the single ^
being reserved for the regular natural »power« operation on proper type
class instances (in Power.thy)
Hence
abbreviation compower :: "'a ⇒ nat ⇒ 'a" (infixr "^^" 80)
where "f ^^ n ≡ compow n f"
was just an idea how you could combine a kind of established power
notation on the syntax level with natural argument order on the logical
level – with the drawbacks already hinted in this thread included.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 17:48):From: Lars Hupel <hupel@in.tum.de>
Hi Florian,
well, referring to Isabelle2018-RC0, compow is and ad-hoc overloaded
constants:
this is not what I'm referring to. I meant
"HOL-Library.Adhoc_Overloading".
Cheers
Lars
Email Gateway (Aug 22 2022 at 17:48):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lars,
this is not what I'm referring to. I meant "HOL-Library.Adhoc_Overloading".
I see now.
So far we have be reluctant to include that theory into Main since all
those user-space type system mechanisms (type class parameters, ad-hoc
overloading, something more I don't quite recall at the moment) are
somehow divergent in their applications and don't interact so smoothly.
Maybe we could have a chat on that on my next visit to TUM.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 17:51):From: Lars Hupel <hupel@in.tum.de>
Maybe we could have a chat on that on my next visit to TUM.
We have talked about this and it's probably not a good idea to include
ad-hoc overloading into HOL or even Pure, even though many users will
have it imported transitively somehow anyway.
A more pragmatic way of getting rid of that particular instance of
overloading might instead be to just disambiguate the syntax.
Many other operations on relations are written as superscripts, where
the set operation is one superscript and the function operation two (cf
trancl/tranclp).
It suffices to find a sufficiently hat-like symbol, e.g.
text ‹‹R ⇧^ n››
text ‹‹R ⇧^⇧^ n››
or
text ‹‹R ⇧△ n››
text ‹‹R ⇧△⇧△ n››
Any opinions?
Cheers
Lars
Email Gateway (Aug 22 2022 at 17:51):From: Lars Hupel <hupel@in.tum.de>
For posterity, I will try to document the cause of the problem. To
people familiar with dependency tracking in the kernel, this will
probably all be obvious.
First, consider a stripped-down example.
no_notation compower (infixr "^^" 80)
consts compow :: "nat ⇒ 'a ⇒ 'a"
abbreviation compower :: "'a ⇒ nat ⇒ 'a" (infixr "^^" 80)
where "f ^^ n ≡ compow n f"
overloading
funpow ≡ "compow :: nat ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)"
begin
primrec funpow :: "nat ⇒ ('a ⇒ 'a) ⇒ 'a ⇒ 'a"
where
"funpow 0 f = id"
| "funpow (Suc n) f = f ∘ funpow n f"
end
definition foo where
"foo f n = (f :: 'a ⇒ 'b) ^^ n"
This definition is rejected with a similar message ("malformed
dependency"), that comes deep from inside the machine room ("defs.ML").
"foo" is trying to depend on "f", but in such a way that neither
a) "f" is fully polymorphic ("nat ⇒ 'a ⇒ 'a") nor
b) "f" is fully instantiated (e.g. "nat ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)").
Hence, it is unclear on what logical entity "foo" should depend on. In
particular, the type of "funpow" is an instance of the type of "compow"
as it is used in the definition "foo".
Admitting just that definition wouldn't be problematic. But admitting a
definition "bar" that uses "foo" could then potentially restrict the
type of "foo", introducing a dependency that isn't tracked otherwise.
Email Gateway (Aug 22 2022 at 18:14):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
This is also on my abstract agenda for a couple of years now.
The key observation is that there are (at least) three concepts
which are nearly the same but implemented separately an presumably
divergently, and hence not very likely to interact smoothly.
Florian
signature.asc
Email Gateway (Aug 22 2022 at 18:14):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
This is what I also prefer – the current state of affairs appears to use
an intricate logical concept (overloading) just for the purpose of notation.
Florian
signature.asc
Email Gateway (Aug 22 2022 at 18:15):From: Tobias Nipkow <nipkow@in.tum.de>
On 10/08/2018 14:09, Florian Haftmann wrote:
For posterity, I will try to document the cause of the problem. To
people familiar with dependency tracking in the kernel, this will
probably all be obvious."foo" is trying to depend on "f", but in such a way that neither
a) "f" is fully polymorphic ("nat ⇒ 'a ⇒ 'a") nor
b) "f" is fully instantiated (e.g. "nat ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)").Hence, it is unclear on what logical entity "foo" should depend on. In
particular, the type of "funpow" is an instance of the type of "compow"
as it is used in the definition "foo".Admitting just that definition wouldn't be problematic. But admitting a
definition "bar" that uses "foo" could then potentially restrict the
type of "foo", introducing a dependency that isn't tracked otherwise.I see this complexity -- inherited from distant past -- as a motivation
to do away with overloading of funpow/compow. Instead it could be either
done with abstract syntax (adhoc_overloading) or concrete syntax (notation).This is what I also prefer – the current state of affairs appears to use
an intricate logical concept (overloading) just for the purpose of notation.
A large part of the success of a formalization rests on notation. Hence I would
definitely not want to dilute the current uniform use of ^.
Tobias
Florian
Email Gateway (Aug 22 2022 at 18:15):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
The current use of (^), namely the operation of naturals on monoids, has
never been put into doubt on this thread.
Concerning (^^), my hope is exactly that we can retain that uniform
notation as mere syntax without bending the logical foundations behind
in the middle run.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 18:15):From: Tobias Nipkow <nipkow@in.tum.de>
On 13/08/2018 11:37, Florian Haftmann wrote:
I see this complexity -- inherited from distant past -- as a motivation
to do away with overloading of funpow/compow. Instead it could be either
done with abstract syntax (adhoc_overloading) or concrete syntax
(notation).This is what I also prefer – the current state of affairs appears to use
an intricate logical concept (overloading) just for the purpose of
notation.A large part of the success of a formalization rests on notation. Hence
I would definitely not want to dilute the current uniform use of ^.The current use of (^), namely the operation of naturals on monoids, has
never been put into doubt on this thread.
I mistyped.
Concerning (^^), my hope is exactly that we can retain that uniform
notation as mere syntax without bending the logical foundations behind
in the middle run.
Then I am all for it.
Tobias
Cheers,
Florian
Last updated: Apr 25 2024 at 01:08 UTC