Email Gateway (Aug 19 2022 at 17:07): Email Gateway (Aug 19 2022 at 17:07):From: Larry Paulson <lp15@cam.ac.uk>
I would like to discuss the question of overloading on fact, the factorial function.
Currently, this function (introduced in src/HOL/Fact.thy) is overloaded, with separate but equivalent definitions on the natural numbers and the integers. The domain of the factorial function is extended to negative integers like this:
"fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
The point of the overloading is to allow fact to be used in both int and nat contexts. However, Isabelle now provides automatic coercions between types. This removes the original motivation while introducing a significant drawback: an occurrence of the function fact in an arithmetical context now becomes ambiguous, and it is possible to get equivalent-looking formulas that have different instances of the function fact, with implicit coercions making the types work out. But such formulas are not equal.
I would like to propose removing the overloading on the factorial function and having the natural number version only. The natural numbers are the actual domain of this function, and implicit coercions allow its use or integers or reals are expected.
Comments welcome!
Larry Paulson
Email Gateway (Aug 19 2022 at 17:08):From: Johannes Hölzl <hoelzl@in.tum.de>
I also second this proposal, the definition of fact_int is quite
strange.
What about defining fact semi-polymorphic? Like
fact :: nat => 'a::semiring_1
then we do not need to depend on coercions, only on typeclasses. And in
semiring_1 the defining fact-equations should hold.
Email Gateway (Aug 19 2022 at 17:08):From: Makarius <makarius@sketis.net>
I have nothing to add concerning overloading, just the plain name: call it
"factorial" (and the theory "Factorial") to say more clearly what it is.
Makarius
Email Gateway (Aug 19 2022 at 17:22):From: Johannes Hölzl <hoelzl@in.tum.de>
Am Samstag, den 28.02.2015, 11:09 +0000 schrieb Larry Paulson:
Presumably for the Fibonacci numbers too? Currently
fun fib :: "nat \<Rightarrow> nat"
where
fib0: "fib 0 = 0"
| fib1: "fib (Suc 0) = 1"
| fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
Hm, I don't know, I would be careful to introduce too much generality.
Even simple rules like "0 <= fact n" or "0 <= fib n" need to be
annotated with a type class constraint.
I made the suggestion for fact as it is used a lot for transcendental
functions.
On 28 Feb 2015, at 08:18, Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de> wrote:
What about defining fact semi-polymorphic? Like
fact :: nat => 'a::semiring_1The nice thing about this is that simple propositions involving numerals
are provable out of the box:context semiring_1
beginprimrec factorial :: "nat ⇒ 'a"
where
"factorial 0 = 1"
| "factorial (Suc n) = of_nat (Suc n) * factorial n"lemma "factorial 3 = 6"
by (simp add: eval_nat_numeral)end
This is again one of the things where you ask yourself how it could have
been different in the past after you got used to it.Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
Email Gateway (Aug 19 2022 at 17:30):From: Peter Lammich <lammich@in.tum.de>
On So, 2015-03-01 at 09:27 +0100, Tobias Nipkow wrote:
On 27/02/2015 17:42, Makarius wrote:
On Fri, 27 Feb 2015, Larry Paulson wrote:
I would like to discuss the question of overloading on fact, the factorial
function.I have nothing to add concerning overloading, just the plain name: call it
"factorial" (and the theory "Factorial") to say more clearly what it is.
I support this - provided we have a nice short syntax for "factorial", ideally
the canonical "!". Maybe it is time to give up the ancient "!" syntax for \<forall>?
As long as the ! does not clash with the binary infix operator ! on
lists, e.g., "a! - b" as "fac a - b" or "nth a (-b)"
Peter
Tobias
Email Gateway (Aug 19 2022 at 17:30):From: Johannes Hölzl <hoelzl@in.tum.de>
Yes, nat + automatic coercion is better!
As a test, I replaced "real (fact" by "(fact" in
Transcendental and it works with one exception
(which has the wrong type: "2 * 2 ^ n ≤ real (fact (n + 2))").
Dmitriy did a very good job :-)
Email Gateway (Aug 22 2022 at 09:00):From: Makarius <makarius@sketis.net>
On Mon, 2 Mar 2015, Manuel Eberl wrote:
My experiments yesterday seemed to indicate that it might work.
That was mixfix ("_ !" 999), but with the default priority 0 for the
argument, it will hardly work at all. It should be probably 1000.
Concrete syntax always needs some careful planning, and systematic
inspection of existing grammars. It should be easy to look through all
mixfix declarations in Isabelle examples and AFP applications that mention
"!" -- with the help of a little instrumentation in Pure. Then it is
possible to see which changes have a chance to work.
The \<bold>! thing should work in any case. (Although, ironically,
\<bold>! looks a lot less bold than the regular ! in JEdit)
Maybe a problem with your local configuration. The default IsabelleText
font and the default font-rendering enging (of official Java 7 shipped
with Isabelle) should show a bold "!" as expected.
The Isabelle/jEdit manual has this explanation on Isabelle symbols and the
all-important Isabelle font:
\medskip \paragraph{Font.} Correct rendering via Unicode requires a
font that contains glyphs for the corresponding codepoints. Most
system fonts lack that, so Isabelle/jEdit prefers its own
application font @{verbatim IsabelleText}, which ensures that
standard collection of Isabelle symbols are actually seen on the
screen (or printer).
Note that a Java/AWT/Swing application can load additional fonts only if
they are not installed on the operating system already! Some outdated
version of @{verbatim IsabelleText} that happens to be provided by the
operating system would prevent Isabelle/jEdit to use its bundled version.
This could lead to missing glyphs (black rectangles), when the system
version of @{verbatim IsabelleText} is older than the application version.
This problem can be avoided by refraining to ``install'' any version of
@{verbatim IsabelleText} in the first place, although it is occasionally
tempting to use the same font in other applications.
If that is not the problem, it might be the slightly odd font-rendering
engine of some OpenJDK versions, if you happen to use one. (This requires
manual tinkering in the first place, because standard Oracle Java is
always the default in Isabelle.)
Makarius
Email Gateway (Aug 22 2022 at 09:00):From: Makarius <makarius@sketis.net>
That is a question of input methods in the Prover IDE. In Isabelle2014,
the default etc/symbols provides various input abbreviations that resemble
traditional ASCII replacement syntax, e.g. "!" for "\<forall>" and "-->"
for "\<longrightarrow>". Thus the C+b key sequence in Isabelle/jEdit can
be used to upgrade old sources manually.
When the Prover IDE supports "refactoring" of traditional syntax into
proper Isabelle symbol syntax directly, the above coincidence of input
methods and input syntax may disappear: one could reconsider the input
abbreviations from scratch. Although I felt nostalgic about certain
character sequences when doing this, in allowing to replace the really
ancient Un by \<union>, for example.
Once we are actually there with the IDE support, one could resolve the
delicate question which input abbreviations are provided by default by
easier user configuration of the same. (Presently it requires manual
editing of etc/symbols files and a reboot of the PIDE.)
Makarius
Email Gateway (Aug 22 2022 at 09:01):From: Makarius <makarius@sketis.net>
The Isabelle/jEdit manual has a long explanation on completion. The above
case falls under "Input events" for "syntax keywords" (because some
alphabetic text is to be replaced). It says:
\item Completion of syntax keywords requires at least 3 relevant
characters in the text.
Explicit completion always works, regardless of the input length.
Anyway, I consider the replacements of ALL, EX etc. as very nostalgic.
Makarius
Email Gateway (Aug 22 2022 at 09:01):From: Makarius <makarius@sketis.net>
I am generally in favour of removing the old ASCII variants of well-known
Pure and HOL syntax, but it will probably also take a few more years get
there. (The Prover IDE could eventually provide systematic support for
this.)
Having "!" as prefix operator (all), infix operator (nth), and postfix
operator (factorial) might or might not work, depending of the chosen
syntactic priorities. Note that one also needs to consider robustness in
case of bad or partial input, i.e. the potential for user confusion due to
errors.
We also have brute-force disambiguation via type-inference for tough
cases, but I don't like that very much -- it has caused a lot of technical
problems over the years.
A more defensive notation could use \<^bold>! instead, which is easy to
type in Isabelle/jEdit, at least for people who know how to type it.
Makarius
Email Gateway (Aug 22 2022 at 09:01):From: Makarius <makarius@sketis.net>
IIRC, Isabelle92 or Isabelle93 had possibilities to change concrete syntax
depending on the Pure/HOL type of the expression. But it was not exactly
right in the parser implementation, and there was a conceptual mismatch
with Hindley-Milner type-inference. Thus it disappeared a bit later, and
got replaced by the built-in disambiguation of parsed results via
type-inference (which can cause huge blow-up of possibilities, and
user-confusion in situations of syntax error).
BTW, as far as I can tell, the current isar-ref and implementation manuals
explain the (complex) syntax layers of Isabelle quite faithfully, although
it is a long and entangled way through all of it.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC