Re: [isabelle] extending well-founded partial orders to total well-founded orders



Dear Christian, Andreas and Larry,  

I do not think the proof is trivial, since, as far as I see, Larry's proof idea would need to be applied in several steps in order to avoid conflicts.  

Andreas's proof does not seem easily adaptable here, since wellfoundedness is not closed under unions of arbitrary chains.  The proof from the link Adreas pointed to sounds like a correct implementation of Larry's idea.  

Here is my construction, which is a variation of the one from the blog. (I shall only use the fact that the original relation R is wellfounded.)

Imagine R as a forest, having the minimal elements as roots of the trees and having the branches of the trees possibly crossing each other.  We traverse this forest in a breadth-first way by transfinite induction and wellorder it "on levels" by performing the following steps on a state consisting of a wellorder W.  

1) Start with W = {}

2) In the successor case: Get the set M of minimal elements of R that are not in (the field of) W, and let V be a well-order on M. Take W' to be the concatenation (ordinal sum) of W and V.  

3) In the limit case: Take the union: the result is a wellorder, since the chain involved in the union has the property that each element is not only a subset, but also an initial segment of any later one.  

The final W has exhausted the whole R, hence it is the desired wellorder.  

My AFP formalization ordinals

http://afp.sourceforge.net/entries/Ordinals_and_Cardinals.shtml

(hopefully) provides the necessary ingredients: Initial segments in Wellorder_Embedding, ordinal sum in theory Constructions_on_Wellorders, and a transfinite recursion combinator (a small adaptation of the wellfounded combinator) in theory Wellorder_Relation. 

Best regards, 
   Andrei 




--- On Fri, 1/18/13, cl-isabelle-users-request at lists.cam.ac.uk <cl-isabelle-users-request at lists.cam.ac.uk> wrote:

From: cl-isabelle-users-request at lists.cam.ac.uk <cl-isabelle-users-request at lists.cam.ac.uk>
Subject: Cl-isabelle-users Digest, Vol 91, Issue 14
To: cl-isabelle-users at lists.cam.ac.uk
Date: Friday, January 18, 2013, 8:13 AM

Send Cl-isabelle-users mailing list submissions to
    cl-isabelle-users at lists.cam.ac.uk

To subscribe or unsubscribe via the World Wide Web, visit
    https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users
or, via email, send a message with subject or body 'help' to
    cl-isabelle-users-request at lists.cam.ac.uk

You can reach the person managing the list at
    cl-isabelle-users-owner at lists.cam.ac.uk

When replying, please edit your Subject line so it is more specific
than "Re: Contents of Cl-isabelle-users digest..."


Today's Topics:

   1. Re:  Trying to use "datatype" to restrict types of formulas
      used, getting error (Gottfried Barrow)
   2. Re:  extending well-founded partial orders to total
      well-founded orders (Christian Sternagel)
   3. Re:  extending well-founded partial orders to total
      well-founded orders (Christian Sternagel)
   4. Re:  Trying to use "datatype" to restrict types of formulas
      used, getting error (Gottfried Barrow)
   5. Re:  Trying to use "datatype" to restrict types of    formulas
      used, getting error (John Wickerson)
   6.  TAP 2013: Final Call for Papers (Achim D. Brucker)
   7. Re:  Trying to use "datatype" to restrict types of formulas
      used, getting error (Gottfried Barrow)


----------------------------------------------------------------------

Message: 1
Date: Thu, 17 Jan 2013 14:25:04 -0600
From: Gottfried Barrow <gottfried.barrow at gmx.com>
Subject: Re: [isabelle] Trying to use "datatype" to restrict types of
    formulas used, getting error
To: cl-isabelle-users at lists.cam.ac.uk
Message-ID: <50F85E20.2060301 at gmx.com>
Content-Type: text/plain; charset=UTF-8; format=flowed

On 1/17/2013 2:12 PM, Gottfried Barrow wrote:
> function sFOLf :: "sFOLdt => bool" where

Please change "function" to "fun".

It still works out the same. Without the "Forall" lines in my "datatype" 
and "fun", my sFOLf function terminates correctly with the message 
"Found termination order: "{}"".

Thanks,
GB




------------------------------

Message: 2
Date: Fri, 18 Jan 2013 13:12:01 +0900
From: Christian Sternagel <c.sternagel at gmail.com>
Subject: Re: [isabelle] extending well-founded partial orders to total
    well-founded orders
To: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
Cc: isabelle-users <isabelle-users at cl.cam.ac.uk>
Message-ID: <50F8CB91.5080003 at gmail.com>
Content-Type: text/plain; charset=UTF-8; format=flowed

Dear Andreas,

thanks for the pointer? I will have a look (however, well-foundedness is 
essential for me).

On 01/17/2013 04:39 PM, Andreas Lochbihler wrote:
> Dear Christian,
>
> I haven't seen a formalisation of that proof, but I have formalised a
> proof that every partial order can be extended to a total order (in the
> appendix, works with Isabelle2012). A preliminary version thereof is
> part of JinjaThreads in the AFP (theory MM/Orders), but I have already
> removed that from the development version, because I no longer need it.
> As you can see there, it is not necessary to modify Zorn.thy from
> Isabelle's library, because you can encode the carrier set in the relation.
>
> For the case of well-foundedness, I found the following informal proof
> in a blog, though I haven't checked whether it is correct:
> http://tylerneylon.com/blog/2007/06/every-well-founded-partial-order-can-be.html
That was also the first "proof" I found via google... but I did not have 
a closer look, since it was "just a blog" :)
>
> It uses the existence of a well-ordering on any set. I don't know
> whether that has been proven in Isabelle before. Andrei might have done
> so in his Cardinals development; he might tell you more.
Isn't that proved at the and of Zorn.thy, lemmas well_ordering and 
well_oder_on?

cheers

chris

>
> Andreas
>
>
> On 01/17/2013 07:55 AM, Christian Sternagel wrote:
>> Dear all,
>>
>> is anybody aware of an Isabelle formalization of the (apparently
>> well-known) fact that every well-founded partial order can be extended
>> to a total well-founded order (in particular a well-partial-order)?
>>
>> If not, any pointers to "informal" proofs (i.e., papers or textbooks ;)).
>>
>> cheers
>>
>> chris
>>
>




------------------------------

Message: 3
Date: Fri, 18 Jan 2013 13:15:17 +0900
From: Christian Sternagel <c.sternagel at gmail.com>
Subject: Re: [isabelle] extending well-founded partial orders to total
    well-founded orders
To: Lawrence Paulson <lp15 at cam.ac.uk>
Cc: isabelle-users <isabelle-users at cl.cam.ac.uk>
Message-ID: <50F8CC55.5010409 at gmail.com>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed

Dear Larry,

thanks for the reply. "is trivial" sounds great. Is a formalization also 
trivial (or even done already)? (Note that I have to extend an existing 
well-founded partial order, not just obtain any total well-order ... I 
mention this only because I did not get the comment about the empty 
relation being well-founded [since I do not start from the empty relation]).

cheers

chris

On 01/17/2013 08:14 PM, Lawrence Paulson wrote:
> This obviously requires the axiom of choice (after all, the empty relation is well-founded), and is trivial with it (simply well-order the set of unrelated elements).
> Larry Paulson
>
>
> On 17 Jan 2013, at 06:55, Christian Sternagel <c.sternagel at gmail.com> wrote:
>
>> Dear all,
>>
>> is anybody aware of an Isabelle formalization of the (apparently well-known) fact that every well-founded partial order can be extended to a total well-founded order (in particular a well-partial-order)?
>>
>> If not, any pointers to "informal" proofs (i.e., papers or textbooks ;)).
>>
>> cheers
>>
>> chris
>>
>




------------------------------

Message: 4
Date: Thu, 17 Jan 2013 22:35:26 -0600
From: Gottfried Barrow <gottfried.barrow at gmx.com>
Subject: Re: [isabelle] Trying to use "datatype" to restrict types of
    formulas used, getting error
To: cl-isabelle-users at lists.cam.ac.uk
Message-ID: <50F8D10E.9000502 at gmx.com>
Content-Type: text/plain; charset=UTF-8; format=flowed

People can ignore what I was talking about, unless someone wants to give 
me a complete "datatype" and "fun/primrec" solution based on the 
informal, recursive definition I gave. Or a solution of another form 
would be okay.

Trying to figure out how recursion works, I have this experimental code:

typedecl sT
consts inS :: "sT => sT => bool" (infixl "inS" 55)

datatype sFOLdt =
   In     sT sT
  |And    bool bool
  |Rec    bool

primrec sFOLf :: "sFOLdt => bool" where
   "sFOLf (In u1 u2)   = (u1 inS u2)"                           |
   "sFOLf (And f1 f2)  = ((sFOLf (Rec f1)) & (sFOLf (Rec f2)))" |
   "sFOLf (Rec f)      = True"

which gives the error: Extra variables on rhs: "(sFOLf::(sFOLdt => bool))"

All that to say, trial and error has shown me I haven't understood 
certain basic things, but trial and error can be an excellent learning 
aid sometimes.

Regards,
GB



------------------------------

Message: 5
Date: Fri, 18 Jan 2013 06:35:10 +0100
From: John Wickerson <jpw48 at cam.ac.uk>
Subject: Re: [isabelle] Trying to use "datatype" to restrict types of
    formulas used, getting error
To: Gottfried Barrow <gottfried.barrow at gmx.com>
Cc: cl-isabelle-users at lists.cam.ac.uk
Message-ID: <B5EE0B87-2B81-423A-B541-B206AF2AA37E at cam.ac.uk>
Content-Type: text/plain; charset=us-ascii

Hi Gottfried,

The problem is here...

> function sFOLf :: "sFOLdt => bool" where
> ...
> "sFOLf (Forall u f) = (!u. f)"

On the left you have free variables u and f, both of the same status. On the right, u is a binder, and any appearances of u inside f are bound to that binder.

I think things might be improved if you change your datatype from

> datatype sFOLdt =
> ...
> |Forall sT bool

to something like 

> datatype sFOLdt =
> ...
> |Forall "sT => bool"

Then you could write something like

> function sFOLf :: "sFOLdt => bool" where
> ...
> "sFOLf (Forall f) = (!u. f u)"

That said, I haven't tested this in Isabelle, so I might be way off the mark.

Best wishes,
john


------------------------------

Message: 6
Date: Fri, 18 Jan 2013 07:04:50 +0100
From: "Achim D. Brucker" <brucker at spamfence.net>
Subject: [isabelle] TAP 2013: Final Call for Papers
To: isabelle-users at cl.cam.ac.uk
Message-ID: <20130118060450.GA12060 at shinanogawa.brucker.ch>
Content-Type: text/plain; charset=utf-8


(Apologies if you receive this announcement multiple times.)

!LNCS publication is confirmed!

****************************************************
***                                              ***
***  TAP 2013                                    ***
***                                              ***
***  Abstract submission: January 25, 2013       ***
***  Paper submission:    February 1, 2013       ***
****************************************************
***  TAP 2013 solicits both full papers and      ***
***  (industrial) experience/tool papers         ***
***  in combining proofs and (security) testing  ***
****************************************************


CALL FOR PAPERS

7th INTERNATIONAL CONFERENCE ON TESTS AND PROOFS (TAP 2013)
http://www.spacios.eu/TAP2013

Budapest, Hungary, June 18-19, 2013

The TAP conference is devoted to the synergy of proofs and tests, to the
application of techniques from both sides and their combination for the
advancement of software quality.
Testing and proving seem to be contradictory techniques: once you have
proved your program to be correct then additional testing seems
pointless; on the other hand, when such a proof in not feasible, then
testing the program seems to be the only option. This view has dominated
the research community since the dawn of computer science, and has
resulted in distinct communities pursuing the seemingly orthogonal
research areas.

However, the development of both approaches has lead to the discovery of
common issues and to the realization of potential synergy. Perhaps, use
of model checking in testing was one of the first signs that a
counterexample to a proof may be interpreted as a test case. Recent
breakthroughs in deductive techniques such as satisfiability modulo
theories, abstract interpretation, and interactive theorem proving, have
paved the way for new and practically effective methods of powering
testing techniques. Moreover, since formal, proof-based verification is
costly, testing invariants and background theories can be helpful to
detect errors early and to improve cost effectiveness. Summing up, in
the past few years an increasing number of research efforts have
encountered the need for combining proofs and tests, dropping earlier
dogmatic views of incompatibility and taking instead the best of what
each of these software engineering domains has to offer.

The TAP conference aims to bring together researchers and practitioners
working in the converging fields of testing and proving, and will offer
a generous allocation of papers, panels and informal discussions.

Topics of interest cover theory definitions, tool constructions and
experimentations, and include (other topics related to TAP are welcome):
- Bridging the gap between concrete and symbolic techniques, e.g. using
  proof search in satisfiability modulo theories solvers to enhance
  various testing techniques
- Transfer of concepts from testing to proving (e.g., coverage criteria)
  and from proving to testing
- Program proving with the aid of testing techniques
- New problematics in automated reasoning emerging from specificities of
  test generation
- Verification and testing techniques combining proofs and tests
- Generation of test data, oracles, or preambles by deductive techniques
  such as: theorem proving, model checking, symbolic execution,
  constraint logic programming
- Model-based testing and verification
- Generation of specifications by deduction
- Automatic bug finding
- Debugging of programs combining static and dynamic analysis
- Formal frameworks
- Tool descriptions and experience reports
- Case studies combining tests and proofs
- Domain specific applications of testing and proving to new application
  domains such as validating security protocols, vulnerability detection
  of programs, security

Important Dates:
================
Abstract submission:   January 25, 2013
Paper submission:      February 1, 2013
Notification:          March 3, 2013
Camera ready version:  April 5, 2013
TAP conference:        June 17-21, 2013

Program Chairs:
===============
Margus Veanes (Microsoft Research, USA)
Luca Vigano` (University of Verona, Italy)

Program Committee:
==================
Paul Ammann
Dirk Beyer
Achim D. Brucker
Robert Claris?
Marco Comini
Catherine Dubois
Juhan Ernits
Gordon Fraser
Angelo Gargantini
Christoph Gladisch
Martin Gogolla
Arnaud Gotlieb
Wolfgang Grieskamp
Reiner H?hnle
Bart Jacobs
Thi?rry Jeron
Jacques Julliand
Gregory Kapfhammer
Nikolai Kosmatov
Victor Kuliamin
Michael Leuschel
Karl Meinke
Alexandre Petrenko
Holger Schlingloff
T.H. Tse
Margus Veanes (co-chair)
Luca Vigan? (co-chair)
Burkhart Wolff
Fatiha Zaidi

Submission:
===========
Please submit your papers via easychair
https://www.easychair.org/conferences/?conf=tap2013

TAP 2013 will
accept two types of papers:

- Research papers: full papers with at most 16 pages in LNCS format
  (pdf), which have to be original, unpublished and not submitted
  elsewhere.

- Short contributions: work in progress, (industrial) experience
  reports or tool demonstrations, position statements; an extended
  abstract with at most 6 pages in LNCS format (pdf) is expected.

Accepted papers will be published in the Springer LNCS series
and will be available at the conference.

The contents of previous TAP proceedings is available at:
http://www.informatik.uni-trier.de/~ley/db/conf/tap/

-- 
Dr. Achim D. Brucker, SAP AG, Vincenz-Priessnitz-Str. 1, D-76131 Karlsruhe
           Phone: +49 6227 7-52595, http://www.brucker.ch/



------------------------------

Message: 7
Date: Fri, 18 Jan 2013 00:13:43 -0600
From: Gottfried Barrow <gottfried.barrow at gmx.com>
Subject: Re: [isabelle] Trying to use "datatype" to restrict types of
    formulas used, getting error
To: cl-isabelle-users at lists.cam.ac.uk
Message-ID: <50F8E817.5080005 at gmx.com>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed

On 1/17/2013 11:35 PM, John Wickerson wrote:
> The problem is here...
>> function sFOLf :: "sFOLdt =>  bool" where
>> ...
>> "sFOLf (Forall u f) = (!u. f)"
> [...]
> That said, I haven't tested this in Isabelle, so I might be way off the mark.
John,

No, you're on the mark. Thanks for the tip. That gets rid of that 
particular error, but there are some major problems still. I'm not doing 
any real recursion. Like for this statement,

"sFOLf (And f1 f2)  = (f1 & f2)",

I would need to recurse on f1 and f2, but I'm not even close; that's all 
messed up. I get an error from trying

value "sFOLf (And True True)"

Alfio pointed out section 2.5.6 of the tutorial, page 19:

http://isabelle.in.tum.de/website-Isabelle2012/dist/Isabelle2012/doc/tutorial.pdf

Thanks,
GB



End of Cl-isabelle-users Digest, Vol 91, Issue 14
*************************************************




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.