Re: [Hol-info] HOL Light set comprehensions
Thanks, Rob! Can you explain how HOL4 performs the quantification with GSPEC?
I would think that GSPEC would have to choose a fresh variable, and I've never
understood how that's to be done, because you have know that your new fresh
variable hasn't already been chosen. So I would think that the HOL Light
method of having the parser choose the fresh variable was defensible.
GSPEC : ('a -> 'b # bool) -> 'b -> bool with (essentially) the
following defining property:
GSPEC f v = ?x. f x = (v, T)
So it's GSPEC that chooses the fresh variable, because we need x to not be free
in v, right?
and then the parser translates {y + 6 | y < 0} into GSPEC(\y.(y + 6, y <
0)).
How does GSPEC know to use the same variable y?
In HOL Light there is a constant called GSPEC, but it is just the
identify function,
Thanks! I had wondered about the sets.ml definition:
let GSPEC = new_definition
`GSPEC (p:A->bool) = p`;;
the semantics of the set comprehension are given by something
called SETSPEC, which has to appear in a context where a variable
representing a candidate for membership of the set comprehension is
in scope.
Could you clarify? Here's the sets.ml definition, which I would like to
understand:
let SETSPEC = new_definition
`SETSPEC v P t <=> P /\ (v = t)`;;
As I posted before, SETSPEC is used by parser.ml to create set abstractions
let v = pgenvar() in
let bod = itlist (curry pmk_exists) bvs
(Combp(Combp(Combp(Varp("SETSPEC",dpty),v),babs),fabs)) in
Combp(Varp("GSPEC",dpty),Absp(v,bod))
and I'd really like to understand this, as well as everything else in parser.ml.
Perhaps I can elaborate. My RichterHilbertAxiomGeometry/readable.ml does I
think a nice job of allowing readable HOL Light proofs, with a minimum of type
annotations, double-quotes and back-quotes. Basically it's a version of
Freek's miz3 that allows full use of tactics like REWRITE_TAC. I'm pretty
happy with it, but I wonder if I couldn't substitute some straightforward camlp
parsing for the exec I'm borrowing from update_database.ml. So my first task
is the understand parser.ml.
--
Best,
Bill
--
Rapidly troubleshoot problems before they affect your business. Most IT
organizations don't have a clear picture of how application performance
affects their revenue. With AppDynamics, you get 100% visibility into your
Java,.NET, & PHP application. Start your 15-day FREE TRIAL of AppDynamics Pro!
http://pubads.g.doubleclick.net/gampad/clk?id=84349831&iu=/4140/ostg.clktrk
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Deadline extended: FLOPS 2014 call for papers
** NEWS: Submission deadline extended. - Title, abstract, and draft paper by December 13, 2013 - Full paper by December 15, 2013 (23:59 anywhere in the world) ** Call For Papers === Twelfth International Symposium on Functional and Logic Programming (FLOPS 2014) June 4-6, 2014 Kanazawa, Japan http://www.jaist.ac.jp/flops2014/ -- - Journal publications in JFP (Jounral of Functional Programming) and TPLP (Theory and Practice of Logic Programming) are planned (see below). - Hyakumangoku Matsuri ( https://www.google.com/search?q=hyakumangoku%20matsuri&tbm=isch ) is scheduled *just* after FLOPS 2014. -- FLOPS is a forum for research on all issues concerning declarative programming, including functional programming and logic programming, and aims to promote cross-fertilization and integration between the two paradigms. Previous FLOPS meetings were held at Fuji Susono (1995), Shonan Village (1996), Kyoto (1998), Tsukuba (1999), Tokyo (2001), Aizu (2002), Nara (2004), Fuji Susono (2006), Ise (2008), Sendai (2010), and Kobe (2012). Topics == FLOPS solicits original papers in all areas of functional and logic programming, including (but not limited to): - Language issues: language design and constructs, programming methodology, integration of paradigms, interfacing with other languages, type systems, constraints, concurrency and distributed computing. - Foundations: logic and semantics, rewrite systems and narrowing, type theory, proof systems. - Implementation issues: compilation techniques, memory management, program analysis and transformation, partial evaluation, parallelism. - Applications: case studies, real-world applications, graphical user interfaces, Internet applications, XML, databases, formal methods and model checking. The proceedings will be published as an LNCS volume. The proceedings of the previous meetings (FLOPS 1999, 2001, 2002, 2004, 2006, 2008, 2010, and 2012) were published as LNCS 1722, 2024, 2441, 2998, 3945, 4989, 6009, and 7294. PC Co-Chairs Michael Codish (Ben-Gurion University of the Negev) Eijiro Sumii (Tohoku University) PC Members == Lars Birkedal (Aarhus University) Michael Codish (Ben-Gurion University of the Negev) [co-chair] Marina De Vos (University of Bath) Moreno Falaschi(Universita degli studi di Udine) Carsten Fuhs (University College London) John Gallagher (Roskilde Universitet / IMDEA Software Institute) Samir Genaim (Universidad Complutense de Madrid) Laura Giordano (Universita del Piemonte Orientale) Ichiro Hasuo (University of Tokyo) Fritz Henglein (University of Copenhagen) Andy King (University of Kent) Oleg Kiselyov Vitaly Lagoon (MathWorks) Shin-Cheng Mu (Academia Sinica) Keiko Nakata (Institute of Cybernetics at Tallinn University of Technology) Luke Ong (University of Oxford) Peter Schachte (University of Melbourne) Takehide Soh (Kobe University) Eijiro Sumii (Tohoku University) [co-chair] Tachio Terauchi(Nagoya University) Joost Vennekens(KU Leuven) Janis Voigtlaender (Universitaet Bonn) Stephanie Weirich (University of Pennsylvania) Local Chair === Yuki Chiba (JAIST) Submission == Submissions must be unpublished and not submitted for publication elsewhere. Work that already appeared in unpublished or informally published workshops proceedings may be submitted. See also ACM SIGPLAN Republication Policy: http://www.sigplan.org/Resources/Policies/Republication Submissions should fall into one of the following categories: - Regular research papers: they should describe new results and will be judged on originality, correctness, and significance. - System descriptions: they should contain a link to a working system and will be judged on originality, usefulness, and design. - Declarative pearls: new and excellent declarative programs or theories with illustrative applications. System descriptions and declarative pearls must be explicitly marked as such in the title. Submissions must be written in English and can be up to 15 pages long including references, though pearls are typically shorter. Authors are required to use LaTeX2e and the Springer llncs class file, available at: http://www.springer.de/comp/lncs/authors.html Regular research papers should be supported by proofs and/or experimental results. In case of lack of space, this supporting information should be made accessible otherwise (e.g., a link to a Web page, or an appen
[Hol-info] How to define Double integral
I just want to define a Double integral like "integral (c,d)(\y. integral(a, b)(\x. f x * y))" this define just can do on HOL4, but can't compute the internal integral,because the \x. belong to from negative infinity to positive infinity,but the variable of internal integral just belong to (a,b). So it's not equal,someone can help me ~very thanks! -- Rapidly troubleshoot problems before they affect your business. Most IT organizations don't have a clear picture of how application performance affects their revenue. With AppDynamics, you get 100% visibility into your Java,.NET, & PHP application. Start your 15-day FREE TRIAL of AppDynamics Pro! http://pubads.g.doubleclick.net/gampad/clk?id=84349831&iu=/4140/ostg.clktrk___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Classical Logic and Computation 2014 in Wien - First Call for Papers
-- -- First Call for Papers -- -- International Workshop on Classical Logic and Computation (CL&C'14) http://www.doc.ic.ac.uk/~svb/CL&C14 July, 13 2014 Vienna, Austria CL&C'14 is a satellite workshop of CSL-LICS'14. IMPORTANT DATES Deadline for abstract: April 4, 2014 Deadline for submission:April 11, 2014 Notification of acceptance: June 6, 2014 Final version due: June 25, 2014 Workshop date: July 13, 2014 INTRODUCTION CL&C'14 is the fifth of a conference series on Classical Logic and Computation. It intends to cover all work aiming to explore computational aspects of classical logic and classical proofs in mathematics. This year CL&C will be held as satellite workshop of the joint meeting of CSL and LICS at the Vienna Summer of Logic (http://www.vsl2014.at) CL&C is focused on the interplay between, on one side, the exploration of the computational content of classical mathematical proofs, and on the other side, the languages and the semantical models proposed in computer science for this task: continuations, game models, denotational models, learning models and so forth. The scientific aim of this workshop is to bring together researchers from both proof theory and computer science and to exchange ideas. SCOPE OF CL&C This workshop aims to support a fruitful exchange of ideas between the various lines of research on Classical Logic and Computation. Topics of interest include, but are not limited to: - versions of lambda calculi adapted to represent classical logic; - design of programming languages inspired by classical logic; - cut-elimination for classical systems; - proof representation for classical logic; - translations of classical to intuitionistic proofs; - constructive interpretation of non-constructive principles; - witness extraction from classical proofs; - constructive semantics for classical logic (e.g. game semantics); - case studies (for any of the previous points). SUBMISSION AND PUBLICATION. We have room for informal talks, too. Therefore participants are encouraged to present both: work in progress, overviews of more extensive work, and programmatic / position papers, and completed projects. All submitted papers will be reviewed to normal standards. The PC recognises two kinds of papers: it will distinguish between accepted (full) papers that contain unpublished results not submitted elsewhere, to be published on EPTCS, and presentations of (short) papers about work in progress. The accepted papers will be publised in the open access electronic journal EPTCS. In order to make a submission: - Format your file using the EPTCS (http://style.eptcs.org/) guidelines; there is a 15 page limit. - Use the submission instructions at https://www.easychair.org/conferences/?conf=clc14 PROGRAMME COMMITTEE * Jeremy Avigad (Carnegie Mellon) * José Carlos Espírito Santo (Minho) * Martin Escardo (Edinburgh) * Monika Seisenberger (Swansea) * Paulo Oliva (Queen Mary University of London) - chair * Stefano Berardi (University of Turin) * Steffen van Bakel (Imperial College London) * Thomas Streicher (Darmstadt University) CONTACT PERSON Paulo Oliva -- Rapidly troubleshoot problems before they affect your business. Most IT organizations don't have a clear picture of how application performance affects their revenue. With AppDynamics, you get 100% visibility into your Java,.NET, & PHP application. Start your 15-day FREE TRIAL of AppDynamics Pro! http://pubads.g.doubleclick.net/gampad/clk?id=84349831&iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Call for papers: Nonlinear Reasoning
Special Issue—Journal of Automated Reasoning NONLINEAR REASONING A variety of mature techniques for analyzing systems of linear inequalities have been imported to the domain of automated reasoning. In contrast, techniques for nonlinear functions are still being developed and examined. Nonlinear functions may include polynomials, transcendental functions, solutions to differential equations, and many other classes of functions. Symbolic and numerical methods, and combinations of the two, have been considered. The goal of this special issue is to provide a snapshot of the state of the subject today and the most promising research directions. We welcome submissions that break new ground, as well as those that clarify and explain the central challenges. Examples of suitable topics: • refinements of classical nonlinear decision methods: cylindrical algebraic decomposition, virtual term substitution, Groebner bases, Wu's method • decision procedures for both extensions and fragments of the theory of real closed fields • applications of nonlinear reasoning techniques in mathematics and formal verification • numeric methods, such as interval constraint propagation and homotopy continuation • symbolic-numeric methods • heuristic reasoning methods • integration of nonlinear methods with resolution theorem provers, interactive theorem provers, SMT solvers Papers (no longer than 30 pages) should be submitted via easychair. Special issue editors: Jeremy Avigad (avi...@cmu.edu) and Lawrence C. Paulson (l...@cam.ac.uk) Deadline for submissions: 1 March 2014 http://www.andrew.cmu.edu/user/avigad/JAR_nonlinear.html https://www.easychair.org/account/signin.cgi?conf=jarnonlinear -- Rapidly troubleshoot problems before they affect your business. Most IT organizations don't have a clear picture of how application performance affects their revenue. With AppDynamics, you get 100% visibility into your Java,.NET, & PHP application. Start your 15-day FREE TRIAL of AppDynamics Pro! http://pubads.g.doubleclick.net/gampad/clk?id=84349831&iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
