Re: [Hol-info] How to correctly define a binder (as pretty printer)?
The only easy way to do this at the moment would be to
- Define a fake constant with the name of the binder you want, but which does
nothing. E.g.,
Define`AE x = x`;
- Make it a binder :
set_fixity “AE” Binder;
- Define your real constant as below:
Define`almost_everywhere m P = …`
- Then
associate_restriction ("AE", "almost_everywhere")
Then, you can get the sort of effect you want by writing
``AE x::m. P``
The m will be a free variable, and the x will be bound in P. If you do a
dest_term on it, you will get
COMB(``almost_everywhere m``, ``\x. P``)
In some future update to HOL, I’d like to make it possible to use the
set-membership epsilon instead of the ::, which is not a great piece of syntax.
I hope this helps. I will think about your second question some more.
Michael
On 7/2/17, 07:58, "Chun Tian (binghe)" wrote:
Hi,
Suppose I have the following definition about a predicate P (with a measure
space m):
val almost_everywhere_def = Define `
almost_everywhere m P = ?N. null_set m N /\ !x. x IN (UNIV DIFF N) ==>
P x`;
(I think you can safely think it as `almost_everywhere m P = !x. P x`.)
Now my purpose is to define a syntax "AE x in m. P”, which has the meaning:
``almost_everywhere m (\x. P)``. The main difficulty is that, x is not a free
variable.
If I try to define it in this (wrong) way:
val AE_def = Define `AE x m P = almost_everywhere m (\x. P)`;
val _ = add_rule { term_name = "AE", fixity = Prefix 1000, (* make sure
lower than limit "-->" *)
pp_elements = [ PPBlock ([TOK "AE", BreakSpace(1,2), TM,
BreakSpace(1,0), TOK "in"],
(PP.CONSISTENT, 0)),
BreakSpace(1,2), TM, HardSpace 0, TOK ".",
BreakSpace(1,0) ],
paren_style = OnlyIfNecessary,
block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)) };
A test term like the following looks good but actually not:
> ``AE x in p. (\j. (X_n j x)) --> (X x)``;
<>
val it =
``AE x in p. ((λj. X_n j x) --> X x)``:
term
because somehow the outside “x” is a free variable in this term. So I have
no way to further define my final concept:
val converge_AE_def = Define `converge_AE p X_n X = AE x in p. (\j. (X_n j
x)) --> (X x)`;
Can anyone suggest a correct way to define the “AE” syntax?
P. S. furthermore, is it possible to define a pretty printer for the last
definition “converge_AE p X_n X”, to make it printing into the following form?
X_n --> X (p-a.e.)
Best Regards,
Chun Tian
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, SlashDot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] How to correctly define a binder (as pretty printer)?
Hi,
Suppose I have the following definition about a predicate P (with a measure
space m):
val almost_everywhere_def = Define `
almost_everywhere m P = ?N. null_set m N /\ !x. x IN (UNIV DIFF N) ==> P x`;
(I think you can safely think it as `almost_everywhere m P = !x. P x`.)
Now my purpose is to define a syntax "AE x in m. P”, which has the meaning:
``almost_everywhere m (\x. P)``. The main difficulty is that, x is not a free
variable.
If I try to define it in this (wrong) way:
val AE_def = Define `AE x m P = almost_everywhere m (\x. P)`;
val _ = add_rule { term_name = "AE", fixity = Prefix 1000, (* make sure lower
than limit "-->" *)
pp_elements = [ PPBlock ([TOK "AE", BreakSpace(1,2), TM,
BreakSpace(1,0), TOK "in"],
(PP.CONSISTENT, 0)),
BreakSpace(1,2), TM, HardSpace 0, TOK ".",
BreakSpace(1,0) ],
paren_style = OnlyIfNecessary,
block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)) };
A test term like the following looks good but actually not:
> ``AE x in p. (\j. (X_n j x)) --> (X x)``;
<>
val it =
``AE x in p. ((λj. X_n j x) --> X x)``:
term
because somehow the outside “x” is a free variable in this term. So I have no
way to further define my final concept:
val converge_AE_def = Define `converge_AE p X_n X = AE x in p. (\j. (X_n j x))
--> (X x)`;
Can anyone suggest a correct way to define the “AE” syntax?
P. S. furthermore, is it possible to define a pretty printer for the last
definition “converge_AE p X_n X”, to make it printing into the following form?
X_n --> X (p-a.e.)
Best Regards,
Chun Tian
signature.asc
Description: Message signed with OpenPGP using GPGMail
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, SlashDot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] WiL 2017: Women in Logic Workshop Second Call for Papers (new dates)
Second Call for Papers WiL 2017: Women in Logic Workshop Reykjavik, Iceland June 19, 2017 https://sites.google.com/site/firstwomeninlogicworkshop/ NEW * Submissions can be either a paper or a talk abstract. * Extended submission deadline: 31 March 2017 OVERVIEW Affiliated with the Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 20-23 June 2017, Reykjavik, Iceland. We are holding the first Women in Logic (WiL) workshop as a LICS associated workshop this year. The workshop intends to follow the pattern of meetings such as Women in Machine Learning (WiML, http://wimlworkshop.org/) or Women in Engineering (WIE, (http://www.ieee-ras.org/membership/women-in-engineering) that have been taking place for quite a few years. Women are chronically underrepresented in the LICS community; consequently they sometimes feel both conspicuous and isolated, and hence there is a risk that the under-representation is self-perpetuating. The workshop will provide an opportunity for women in the field to increase awareness of one another and one another's work, to combat the feeling of isolation. It will also provide an environment where women can present to an audience comprised of mostly women, replicating the experience that most men have at most LICS meetings; we hope that this will be particularly attractive to early-career women. Topics of interest of this workshop include but are not limited to the usual Logic in Computer Science (LICS) topics. These are listed as automata theory, automated deduction, categorical models and logics, concurrency and distributed computation, constraint programming, constructive mathematics, database theory, decision procedures, description logics, domain theory, finite model theory, formal aspects of program analysis, formal methods, foundations of computability, higher-order logic, lambda and combinatory calculi, linear logic, logic in artificial intelligence, logic programming, logical aspects of bioinformatics, logical aspects of computational complexity, logical aspects of quantum computation, logical frameworks, logics of programs, modal and temporal logics, model checking, probabilistic systems, process calculi, programming language semantics, proof theory, real-time systems, reasoning about security and privacy, rewriting, type systems and type theory, and verification. SUBMISSIONS Contributions should be written in English and can be submitted in the form of full papers (with a maximum of 10 pages), short papers (with a maximum of 5 pages), or talk abstracts (1 page). Papers and abstracts should be prepared in latex using the LICS style (IEEE Proceedings 2-column 10pt). LaTeX style files are available at http://www.ctan.org/tex-archive/macros/latex/contrib/IEEEtran/. Please use IEEEtran.cls version V1.8b, released on 26/08/2015. The submission should be in the form of a PDF file uploaded to the WiL 2017 Easychair page (https://easychair.org/conferences/?conf=wil2017) before the submission deadline of 31 March 2017, anywhere on Earth. PROCEEDINGS We plan to publish a post conference volume at ENTCS or other equally visible outlet. IMPORTANT DATES Paper submission deadline: 31 March 2017 Author notification: 1 May 2017 Contribution for Informal Proceedings: 22 May 2017 INVITED SPEAKERS * Claudia Nalon (University of Brasilia, Brasil) * Catuscia Palamidessi (INRIA Saclay and LIX, France) SCIENTIFIC AND ORGANIZING COMMITTEE * Valeria de Paiva (Chair, Nuance Communications, USA) * Adriana Compagnoni (Stevens Institute of Technology, USA) * Amy Felty (University of Ottawa, Canada) * Anna Ingolfsdottir (Reykjavik University, Iceland) * Ursula Martin (University of Oxford, UK) * Brigitte Pientka (McGill University, Canada) * Alexandra Silva (University College London, UK) * Perdita Stevens (University of Edinburgh, UK) -- Check out the vibrant tech community on one of the world's most engaging tech sites, SlashDot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
