Email Gateway (Aug 18 2022 at 18:34): Email Gateway (Aug 18 2022 at 18:34):From: "gallais @ ensl.org" <guillaume.allais@ens-lyon.org>
Hi everyone,
I did not find Isabelle's bug tracker so I hope that this is the place where
I'm supposed to report this.
Pierre Boutillier's trick (which breaks Coq's SN) seems to work in Isabelle.
As in Agda, we do not lose SN but we do accept a function that is not
well-defined.
================================
theory test
imports Main
begin
fun f :: "unit \<Rightarrow> unit" where
"f x = (\<lambda> _ . ()) (f ())"
lemma fail : "f () \<equiv> ()"
by simp
end
================================
Cheers,
Email Gateway (Aug 18 2022 at 18:34):From: Tobias Nipkow <nipkow@in.tum.de>
There is no bug here. "(% _ . ()) (f ()) = ()", and "f x = ()" is
exactly what Isabelle defines. You can see that when you look at the thm
f.simps. You may complain that Isabelle beta-reduced the rhs of your
input string before it made the definition. You can hide the beta redex
by an explicit apply function, and then fun will no longer accept your
input.
The point is that your input string is transformed into a definition and
on the way it may get modified, and this is unavoidable. Beta-reduction
is one of the possible modifications. Disambiguation on pattern matching
is another.
Tobias
Email Gateway (Aug 18 2022 at 18:34):From: Makarius <makarius@sketis.net>
You quote this like something that is well-known in the constructive
community. Can you point to some mailing list threads discussing it, or
similar?
On his web page, Pierre Boutillier has the following interesting
quotation:
What I cannot create, I do not understand.
Richard Feynman (Merci O. Danvy)
This attitude might explain part of the confusion. Isabelle/HOL is a very
platonistic system, using classical mathematical principles that are not
as "created" as one would expect in Coq or Agda.
As Tobias has already pointed out, our abstract syntax layer works modulo
various reductions (alpha, beta, eta) that are considered a purely
syntactic device on the term language, without any computational idea
behind it. The heavy lifting is then done in classic set-theory of HOL
behind the scenes, so that the original specification of the user is
eventually derived as actual theorems (plus extra infrastructure such as
simplification and induction rules).
Back to the example:
fun f :: "unit => unit" where ...
My first reaction as a classically-mindend person: Isn't there just one
such function "unit => unit", namely "\<lambda>x. ()", so it does not
really matter what the user specifies or the system defines behind the
scenes, the "fail" result always holds universally:
lemma
fixes f :: "unit \<Rightarrow> unit"
shows "f x = ()" by (cases "f x")
But the unit type is not really essential in the "trick". Consider this
variant:
fun g :: "'a \<Rightarrow> 'a" where
"g x = (\<lambda>_. undefined) (g undefined)"
Here "undefined" is just a global unspecified constant that is used as a
dummy here. Equally well you could have written this from the very start:
fun g :: "'a \<Rightarrow> 'a" where
"g x = undefined"
Here we know that "g x" is always that constant, without known what it is.
(It might also depend on the type 'a.) The Isabelle/HOL library has a
slightly more constructive variant of this idea, where some overloaded
constant "default" is the parameter of a type-class of the same name.
Thus the value is usually known from the type structure by extra-logical
means, such that the code generator can use that information, for example.
Makarius
Email Gateway (Aug 18 2022 at 18:34):From: Alexander Krauss <krauss@in.tum.de>
I did not find Isabelle's bug tracker so I hope that this is the place where
I'm supposed to report this.
In principle, yes, although this concrete one is a misunderstanding. (We
currently have no formal tracking of bugs or misunderstandings)
Pierre Boutillier's trick (which breaks Coq's SN) seems to work in Isabelle.
As in Agda, we do not lose SN but we do accept a function that is not
well-defined.
Some further remarks:
You seem to be using a specific notion of "well-defined", probably
coming from constructive type theory.
In HOL, there is no formal notion of well-definedness other than a very
primitive one. Leaving pattern matching aside for now, we should rather
say that a function (given by a recursive equation) is "definable", iff
there is a HOL term that satisfies the equation (here that term is
"\<lambda> _. ()"). Finding that term basically amounts to "solving" the
equation, and this is what the definition command does for you for a
certain subclass of definable functions.
Note also that Isabelle has no notion of SN other than the trivial
beta/eta reduction of simply-typed lambda calculus. In particular,
definitions are not unfolded (aka reduced) automatically, unlike in Coq,
Agda etc. This means that "f is terminating" is merely an informal way
of saying "f can be defined using well-founded induction".
Alex
Email Gateway (Aug 18 2022 at 18:35):From: "gallais @ ensl.org" <guillaume.allais@ens-lyon.org>
Thanks for all the comments: I now understand a bit more the philosophy
behind Isabelle. Given that extraction remains safe (I guess that the simps
equations are the one used to generate the code?), I suppose that this is
just a matter of taste.
Last updated: May 02 2024 at 01:06 UTC