Email Gateway (Aug 19 2022 at 13:00): Email Gateway (Aug 19 2022 at 13:00):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
My ashamed apologizes if this looks as weird as I'm afraid it may looks,
however, this question really tickles me.
I came to something like this after some simplifications, so I wanted to
test it with a lemma:
lemma "f = (λa. a ∨ f a) ⟹ (f a = a)"
Isabelle tells me it found a counter example with “a = False” and “f a =
True” . It does not seems to see there is an infinite recursion, or else I
don't understand how it can believe “f a” may differs from “a” (how so?).
To me, it can only be “a”, an infinite never ending sequence of
disjunctions of the same term may be nothing else if it's ever something,
than this term.
I guess this case looks weird, but I would like to know, first if Isabelle
sees it as an infinitely recursive lambda expression or not, then if if it
do, if there exists some trusted axioms which are able to deal with this?
Email Gateway (Aug 19 2022 at 13:00):From: John Wickerson <johnwickerson@cantab.net>
Hi Yannick,
The counterexample involves having f as the constant "True" function, and then picking "a" to be False. The assumption in your lemma can be rewritten as
∀x. (f(x) = x ∨ f(x))
and this certainly holds when f is the constant "True" function, since both sides of the =-operator are True. But the conclusion of your lemma doesn't hold since f(False) is not False.
Does that help?
john
Email Gateway (Aug 19 2022 at 13:00):From: Yannick <yannick_duchene@yahoo.fr>
On Sat, 14 Dec 2013 11:29:47 +0100, John Wickerson
<johnwickerson@cantab.net> wrote:
Hi Yannick,
Hello John, and thanks for your interest in the question.
The counterexample involves having f as the constant "True" function,
and then picking "a" to be False. The assumption in your lemma can be
rewritten as∀x. (f(x) = x ∨ f(x))
and this certainly holds when f is the constant "True" function, since
both sides of the =-operator are True. But the conclusion of your lemma
doesn't hold since f(False) is not False.Does that help?
I don't know so far, will see if I understand. At least you seem to
confirm Isabelle really understand it as a recursive function application
(I had a doubt on this for a moment).
Why is f(False) not False ? If it's built with False only and only
disjunctions, where could True comes from?
Or else may be my interpretation is wrong: I see it as an infinite
sequence like “x ∨ x ∨ x ∨ x ∨ x ∨ …”.
For the longer story, what I was attempting with this lemma, is to get a
rule for elimination of this particular kind of infinite recursion. A more
general case could be (in my interpretation which may be erroneous, I
don't know so far): let “+” be an operator, let the proposition “a + b =
a” be previously proved to holds, then an infinite sequence like “a + b +
b + b + b + …” may be substituted to “a”; that was the meaning I expected.
May be there is a way to prove it with something like a list induction and
proving the function recursion is like the list recursion on an infinite
list. May be with a list I could say “what ever the length of a + b + b +
b + b + … it will always be a when a + b = a” so the infinite length list
produce the same if it's interpreted as producing anything (already hardly
provable I believe). Just that it's not a list, it's a recursive function
instead. Then I wondered if there exist an axiom for this in any kind of
theory (either that of Isabelle or from foreign theories) or else if it
would be safe to create one, and I'm afraid of creating an axiom which I'm
not able to prove (so a pure axiom, not a theorem).
Email Gateway (Aug 19 2022 at 13:00):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Yannick,
I just make more explicit what John says with regards to the constant
function, and also, explicitly, for any free variables in a lemma, there
is implicit universal quantification of those free variables, something
which Christian Sternagel made explicit enough with explicit examples to
conclusively show, for me, the connection between free variables and
universal quantification.
There can be lots of implicit action working underneath.
You're stating this:
lemma "!!f. !!a. f = (%a. a | f a) ==> (f a = a)"
oops
So, let "f = (%a. True)", and for the quantified variable "a", let "a =
False".
Then
lemma "(%x. True) = (%x. x | (%x. True) x) ==> ((%x. True) False ~= False)"
by(simp)
Regards,
GB
Email Gateway (Aug 19 2022 at 13:00):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m afraid that’s your mistake. Such expressions simply don’t make sense.
Larry Paulson
Email Gateway (Aug 19 2022 at 13:01):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I wanted to check if had an issue with binding (indeed, I did had issues
with implicit operations in some cases), so tried this:
lemma "f = (λa. False ∨ f False) ⟹ (f False = False)"
It still says it find a counter example, with “f False = True”. Precisely,
what I don't understand, is why it suppose this may be True. “a” is not
used, and the only constant used in f is False.
I must be missing something important, or else it's just Auto Quickcheck
which is not made for this kind of infinite expression.
I won't go with an axiom, looks unsafe if I am missing something.
Email Gateway (Aug 19 2022 at 13:01):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I agree opinion may vary about the sense, I mainly had the hope this won't
be unsound.
I will go another way, reformulating some expressions, using a garde, to
avoid this case. The question was still interesting to me.
Thanks again for the comments.
Email Gateway (Aug 19 2022 at 13:01):From: Lawrence Paulson <lp15@cam.ac.uk>
It is simply that if f is the constant-True function, then f = (λa. False ∨ f False).
I think that you are imagining some sort of execution model for HOL. But HOL doesn’t have an operational semantics.
Larry Paulson
Email Gateway (Aug 19 2022 at 13:04):From: Gottfried Barrow <gottfried.barrow@gmx.com>
You might have worked this out already, but I attach and include a THY
which has comments. You're treating "=" as programming language
assignment, but it's not. You're also speaking of non-terminating,
recursive functions, but they don't exist in HOL, so I've read, I think.
In the second half the theory, I define a recursive function, sumXP, and
I demonstrate that "sumXp 4" doesn't automatically get recursively applied.
I could ask, "How do I easily prove theorem "sumXp 4 = 10", without
using the successor form of nat?" But that would put me over my yearly
quota for asking questions.
Regards,
GB
(******************)
theory i131216a__isaU_eq_is_not_assignment
imports Complex_Main ("../../../iHelp/i")
begin
(SHOWING THAT "=" IS HOL.eq, RATHER THAN PROGRAMMING LANGUAGE ASSIGNMENT)
(*
You're treating "=" as if it's assignment or definition, such as "val x
= 1", but
it's not, it's the application of the function HOL.eq::('a => 'a =>
bool), which
has been axiomatized to have certain properties, such as substitution.
The expression "f = (%a. a | f a)" is a statement of function equality,
and the
pertinent theorem is this:
*)
theorem "(f = g) <-> (!x. f x = g x)"
by(rule fun_eq_iff)
(*
To prove your theorem wrong, I only need one function of type (bool =>
bool),
and I choose (%x. True), with the result that "(%x. True) = (%a. a |
(%x. True) a)"
is True by fun_eq_iff. There are only two values, True and False, that
need to
be tested to determine whether (%x. True) is equal to (%a. a | (%x.
True) a).
Also, this shows that there's no recursion, unless for a particular f, f has
been defined to be recursive. Here, it appears I've defined a recursive
function
named fix_f:
*)
function fix_f :: "bool => bool" where
"fix_f a = (%x. x | fix_f x) a"
by(auto)
(*
Of note is that the "=" used is still HOL.eq, which can be seen by
cntl-clicking
on it.
You might think that "(fix_f True)" should return "(True | fix_f True)",
where
if HOL implements a short-circuited or, it would simplify to "True".
You might think that "(fix_f False)" should be an infinite loop, because
the first iteration will return "(False | fix_f False)", and so on, to
infinity.
You can try to use fix_f in theorems, but it's not usable because
termination
hasn't been proved.
Your options for defining recursive functions are function, fun, and
primrec,
none of which will work for fix_f. The applicable documents are
functions.pdf
and isar-ref.pdf.
*)
function fix_g :: "bool => bool" where
"fix_g a = (%x. x | fix_g x) a"
by pat_completeness auto
termination by lexicographic_order
(*ERROR: Unfinished goal "1. False". Could not find lexicographic
termination
order.*)
fun fix_h :: "bool => bool" where
"fix_h a = (%x. x | fix_h x) a"
(ERROR: Same error as for "function".)
primrec fix_i :: "bool => bool" where
"fix_i a = (%x. x | fix_i x) a"
(ERROR: primrec only defines functions that use datatype.)
(*****************)
(SHOWING THAT RECURSIVE FUNCTIONS DON'T GET "COMPUTED" AUTOMATICALLY)
(*****************)
fun sumXp :: "nat => nat" where
"sumXp 0 = 0"
|"sumXp n = n + sumXp(n - 1)"
find_theorems "sumXp"
thm sumXp.simps
(*
Prints the simp rules created for sumXp: sumXp.simps(1), sumXp.simps(2)
*)
value "sumXp 4"
(*
The code generator prints the successor form of 10. Doing an import of
"~~/src/HOL/Library/Code_Target_Nat" will print 10, but the fact that the
successor form is being used is needed information here.
*)
theorem "sumXp 4 = 10"
apply(simp) oops
(*
But simp here doesn't do any magic computation, even though sumXp.simps(1)
and sumXp.simps(2) are automatically declared as simp rules.
*)
theorem "(!!f::(nat => nat). !!a. f = (%x. f x) ==> f a = a) ==> False"
by(auto)
(*
EXAMPLE: This example, similar to yours, will be made concrete with sumXp.
*)
theorem "sumXp = (%x. sumXp x)"
by(rule eta_contract_eq)
(*
Checking that the left-hand side will be true.
*)
theorem "sumXp = (%x. sumXp x) ==> sumXp 4 = 10"
using[[simp_trace]]
apply(simp) oops
(*
After simp is applied, the goal is "sumXp 4 = 10". The RHS hasn't been
simplified any at all. Computations like this are a result of simp rule
substitutions (rewriting), and simp rules are picky.
*)
theorem "sumXp = (%x. sumXp x) ==>
sumXp (Suc (Suc (Suc (Suc 0))))
= (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))"
(*
Happy simp rules make for happy computations...
*)
using[[simp_trace]]
by(simp)
(*
...by means of rewriting. With the right form of natural numbers, the simp
rules can compute what is needed to obtain the necessary "HOL.eq a b ==
True",
the rewriting of which can be seen at the end of the simp trace.
*)
(declare[[simp_trace]])
value "sumXp 4"
(*
Going back, I'd like to see if simp_trace can tell me what simp rule
"value" is
using to compute value "sumXp 4".
It's using the function Num.nat_of_num, which cntl-clicking will take
you to.
It's also using a lot of other rewrite rules.
*)
term "nat_of_num"
theorem "sumXp 4 = 10"
apply(simp add: nat_of_num.simps)
oops
(*
The message is that nat_of_num.simps are duplicate rewrite rules. It will be
easier just to ask what needs to be done to be able to prove a theorem which
uses an expression like "sumXp 4 = 10".
*)
(******************)
end
i131216a__isaU_eq_is_not_assignment.thy
Email Gateway (Aug 19 2022 at 13:04):From: Gottfried Barrow <gottfried.barrow@gmx.com>
So 4 is not equal to 10, but the primary purpose was to show that
nothing automatically happens with function application, such as "sumXp
4", and at most, a sequence of substitutions are made, if things are
done the way I did them. Most important, maybe, is knowing that infinite
recursion can't happen.
Regards,
GB
Email Gateway (Aug 19 2022 at 13:06):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I did not really interpreted this as an assignment, rather as an equality
which in turn allows a substitution, and so, recursively. Ex:
theory Test
imports Main
begin
(* Based on the original proposition which was: "f = (λa. a ∨ f a) ⟹
(f a = a)" *)
lemma "f = (λa. a ∨ f a) ⟹ f = (λa. a ∨ (λa. a ∨ f a) a)" by simp
lemma "f = (λa. a ∨ f a) ⟹ f = (λa. a ∨ (λa. a ∨ (λa. a ∨ f a) a)
a)" by simp
(* And so on… *)
end
That's why I saw an infinite recursion.
I will have a look later in your extensive sample.
Email Gateway (Aug 19 2022 at 13:07):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
To tell it another way, my erroneous interpretation was to believe it was
the same as a definition of “f”, while both an explicit “definition” and a
“fun/function” definition fails with such an expression:
definition f where "f = (λa. a ∨ f a)" (* Isabelle complains “Extra
variables on rhs: "f"”. *)
fun f where "f a = (a ∨ f a)" (* Isabelle complains “Could not find
lexicographic termination order”. *)
For the second case, no way to try with “function”, as that's absolutely
non‑terminating.
So this was like an attempt to define something impossible to Isabelle,
and also after some comments here, something HOL can't deal with. Finally,
in the absence of any real definition, Quickcheck was free to substitute
“f” to whatever it wanted. This should summarize the case.
Email Gateway (Aug 19 2022 at 13:07):From: Lawrence Paulson <lp15@cam.ac.uk>
From a computational point of view, "f a = (a ∨ f a)” must be regarded as undefined, because the recursion is not well-founded. There are logics where you could then prove that f(True)=True and f(False)=undefined.
Larry Paulson
Email Gateway (Aug 19 2022 at 13:07):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Interesting. Just out of curiosity and learn more (really not to use it),
what are the names of these logics?
Email Gateway (Aug 19 2022 at 13:07):From: Lawrence Paulson <lp15@cam.ac.uk>
You could try Isabelle/HOLCF, but I’m not sure how well documented and supported it is.
Larry Paulson
Email Gateway (Aug 19 2022 at 13:07):From: Yannick <yannick_duchene@yahoo.fr>
This document seems a good introduction on LCF vs HOL and the idea of
getting one with the other:
http://csep.hpcc.nectec.or.th/Journals/oup/smj/journals/ed/titles/computer_journal/Volume_38/Issue_02/38.2.pdf/agerholm.pdf
(the one I will read)
For HOL and LCF as an Isabelle theory, this one:
http://www4.in.tum.de/publ/papers/Regensburger_HOLT1995.pdf
(outdated?)
Quote of the abstract of the former:
Last updated: Nov 21 2024 at 12:39 UTC