* Re: Caml-list Digest, Vol 24, Issue 18
[not found] <20070606100003.AA215BC6C@yquem.inria.fr>
@ 2007-06-06 18:27 ` Greg Meredith
0 siblings, 0 replies; only message in thread
From: Greg Meredith @ 2007-06-06 18:27 UTC (permalink / raw)
To: caml-list
[-- Attachment #1: Type: text/plain, Size: 13863 bytes --]
Oliver,
Many thanks for the links to polycontextural logics. My feeling is it will
take me quite some investment to get a feeling for the framework. In the
meantime, there are fairly simple accounts of concurrency with reflection
offering natural logics (without apparent liar's paradox issues, as i
understand them).
At ETAPS 05 i presented two papers on such systems. You can find preprints
here (
http://svn.biosimilarity.com/src/open/papers/trunk/concurrency/rho/ex_nihilo_entcs/ex_nihilo_finco.pdf;
http://svn.biosimilarity.com/src/open/papers/trunk/concurrency/rho/tgc%20lncs/ex_nihilo_logic.pdf).
i did a quick and dirty OCaml implementation (as a way to learn OCaml),
which you can find here (
http://svn.biosimilarity.com/src/open/mirrororrim/rho/trunk/ocaml/).
The approach i took was based on my dissatisfaction with the fact that the
\pi-calculus was dependent on a theory of names; and, names had to have an
effective theory of equality (thus, sneaking in a notion of computation --
which the \pi-calculus was supposedly providing the foundations of). If you
formulate the situation as: given a set (resp. theory) of names, X, the
\pi-calculus generates a set (resp. theory) of processes \Pi(X), then you
can ask if the following domain equation has a solution
- X = \Pi(X)
It does (lots of them). In the first paper cited i presented a minimal
solution (least fixed point). The basic idea is to introduce a notion of
quotation and dequotation. Quotation happens at communication (output
appears higher-order, in that it has a process in subject position, but what
is sent is the code or quote of the process). Likewise, dequotation is
really only interesting at communction time, when it is bound by an input.
(See the paper for the full story.)
In the second paper, i show that the (spatial logic version of the) standard
Hennessy-Milner construction pushes through -- but with a pleasant surprise.
In addition to formulae describing sets of processes, we find formulae
describing sets of names. You get a whole logic of namespaces. One way to
look at it is this: the algebraic operations on names inherited from the
process algebraic combinators give you a pointer arithmetic. Fortunately,
the programmer of such a system is also equipped with a logic that gives
very potent means of reasoning about this pointer arithmetic. (Again, see
the paper for the full story.)
The reflection doesn't just stop at structural reflection. You can provide a
reflective comm rule in which even synchronization -- which is normally
given via name-equality -- is determined by an upper-level reduction of the
processes whose codes are the names being used to synchronize. Amazingly,
this can be shown to be well-founded.
As a final point of interest, the first paper presents an encoding of the
\pi-calculus into the reflective setting, demonstrating that both
replication and the new-operator are syntactic sugar. There is a process
algebraic form of the Y-combinator in the reflective setting that gives you
replication. My co-author and i came up with two different encodings of the
new-operator. His was 'centralized' but more elegant; mine was distributed,
but with more machinery to make it work. But, i also found a 3rd encoding in
which the well-founded recursion of quotation is replaced by
non-well-founded forms. In this case, you obtain an interpretation of new
that is strongly analogous to Galois extensions of a field.
Best wishes,
--greg
On 6/6/07, caml-list-request@yquem.inria.fr <
caml-list-request@yquem.inria.fr> wrote:
>
> Send Caml-list mailing list submissions to
> caml-list@yquem.inria.fr
>
> To subscribe or unsubscribe via the World Wide Web, visit
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> or, via email, send a message with subject or body 'help' to
> caml-list-request@yquem.inria.fr
>
> You can reach the person managing the list at
> caml-list-owner@yquem.inria.fr
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Caml-list digest..."
>
> Today's Topics:
>
> 1. Re: JoCaml Released. (Oliver Bandel)
> 2. Call for papers - IFL 2007 (Michel Mauny)
> 3. Re: re: We should all be forking (Oliver Bandel)
> 4. Re: JoCaml Released. (Oliver Bandel)
> 5. Re: JoCaml Released. (Jon Harrop)
>
>
> ---------- Forwarded message ----------
> From: Oliver Bandel <oliver@first.in-berlin.de>
> To: caml-list@inria.fr
> Date: Wed, 6 Jun 2007 11:00:38 +0200
> Subject: Re: [Caml-list] JoCaml Released.
> On Wed, Jun 06, 2007 at 10:18:15AM +0200, Oliver Bandel wrote:
> > On Mon, Jun 04, 2007 at 10:13:55AM -0400, Joshua D. Guttman wrote:
> > > Oliver Bandel <oliver@first.in-berlin.de> writes:
> > >
> > > >
> > > >
> > > > As far as I know only polycontextural logic can express
> > > > parallel, distributed systems (and selfreference) in a
> > > > complete/total way. So, when join calculus is
> > > > monocontextural (which it is, if it uses the math we all
> > > > have learned) it will be a subsystem of what can be
> > > > expressed with polycontextural logic.
> > > >
> > >
> > > Well, I googled and found the Wikipedia article on Gotthard
> > > Guenther, which talked about trans-Aristotelian logic and
> > > the law of the excluded middle (shades of Korzybski! Were
> > > they connected?).
> > >
> > > But there was no indication what
> > > monocontextural/polycontextural meant, or why only the
> > > latter expresses distribution *completely*.
> > >
> > > Could you give a brief summary, please?
> > [...]
> >
> > I answered to your private maila ddress twice.
> > ...well oooh, I didn't saw you also wrote to this list.
> >
> >
> > I will collect both mails and send it to the list today.
> >
>
>
> ...is it interests other people...
>
> Ciao,
> Oliver
>
>
>
>
> ---------- Forwarded message ----------
> From: Michel Mauny <Michel.Mauny@inria.fr>
> To: caml-list@inria.fr
> Date: Wed, 06 Jun 2007 11:04:12 +0200
> Subject: [Caml-list] Call for papers - IFL 2007
> **********************************************************************
>
> Announcement and Call for Papers for the
>
> 19th International Symposium on
> Implementation and Application of Functional Languages
> IFL 2007
>
> 27th-29th September 2007, Freiburg, Germany
> co-located with ICFP 2007
>
> http://proglang.informatik.uni-freiburg.de/IFL2007/
>
> **********************************************************************
>
> The aim of the IFL symposium is to bring together researchers actively
> engaged in the implementation and application of functional and
> function-based programming languages. The symposium provides an open
> forum for researchers who wish to present and discuss new ideas and
> concepts, work in progress, preliminary results, etc. related
> primarily but not exclusively to the implementation and application of
> functional languages.
>
> Topics of interest include (but are not limited to):
>
> * language concepts
> * type checking
> * compilation techniques
> * (abstract) interpretation
> * generic programming techniques
> * automatic program generation
> * array processing
> * concurrent/parallel programming
> * concurrent/parallel program execution
> * heap management
> * runtime profiling
> * performance measurements
> * debugging and tracing
> * (abstract) machine architectures
> * verification
> * formal aspects
> * tools and programming techniques
>
> Papers on applications or tools demonstrating the suitability of novel
> ideas in any of the above areas and contributions on related
> theoretical work are also welcome. The change of the symposium name
> adding the term "application", introduced in 2004, reflects the
> broader scope IFL has gained over the years.
>
>
> Contributions
>
> Prospective authors are encouraged to submit papers to be published in
> the draft proceedings and present them at the symposium. All
> contributions must be written in English, conform to the
> Springer-Verlag LNCS series format and not exceed 16 pages. The draft
> proceedings will appear as a technical report.
>
> Every attendee of IFL 2007 will have the opportunity to submit a
> revised version of their paper for post-symposium reviewing. As in
> previous years, selected papers will be published by Springer Verlag
> in the Lecture Notes in Computer Science (LNCS) Series.
>
>
> Important Dates
>
> Submission for Draft Proceedings 31 August 2007
> Early Registration Deadline 1 September 2007
> Symposium 27-29 September 2007
> Submission for post-refereeing 2 November 2007
> Notification of acceptance / rejection 14 December 2007
> Submission of camera-ready version 25 January 2008
>
>
> Programme Committee
>
> Peter Achten Radboud University Nijmegen, The Netherlands
> Kenichi Asai Ochanomizu University, Japan
> Manuel Chakravarty The University of New South Wales, Australia
> Olaf Chitil (chair) University of Kent, UK
> Martin Erwig Oregon State University, Oregon, USA
> Marc Feeley Université de Montréal, Canada
> Martin Gasbichler Zühlke Engineering AG, Switzerland
> Kevin Hammond University of St. Andrews, Scotland
> Zoltán Horváth Eötvös Loránd University, Budapest, Hungary
> John Hughes Chalmers University of Technology, Sweden
> Ken Friis Larsen University of Copenhagen, Denmark
> Rita Loogen Philipps-Universität Marburg, Germany
> Michel Mauny ENSTA, France
> Sven-Bodo Scholz University of Hertfordshire, UK
> Clara Segura Universidad Complutense de Madrid, Spain
> Tim Sheard Portland State University, Oregon, USA
> Glenn Strong Trinity College, Dublin, Ireland
> Doaitse Swierstra Utrecht University, The Netherlands
> Malcolm Wallace The University of York, UK
>
>
> Local Organisation
>
> Markus Degen Universität Freiburg, Germany
> Peter Thiemann Universität Freiburg, Germany
> Stefan Wehr Universität Freiburg, Germany
>
>
> Further Information
>
> http://proglang.informatik.uni-freiburg.de/IFL2007/
>
>
> --
> Michel Mauny
>
> ENSTA
> (+33) 1 4552 5388 (ENSTA)
> (+33) 1 3963 5796 (INRIA)
>
>
>
>
> ---------- Forwarded message ----------
> From: Oliver Bandel <oliver@first.in-berlin.de>
> To: caml-list@inria.fr
> Date: Wed, 6 Jun 2007 11:28:40 +0200
> Subject: Re: [Caml-list] re: We should all be forking
> On Tue, Jun 05, 2007 at 03:30:47PM -0700, Christopher Cramer wrote:
> > Jon Harrop:
> > > I believe the performance relies upon the Linux kernel lazily copying
> > > the process. Does OSX also do that?
> >
> > It's called copy-on-write and I would be surprised if OSX didn't also
> > do it.
> >
> > The only way to start a new process is to fork, so even if you're just
> > running another program you fork first, and then replace the process
> > image with the new program with exec. If the fork had to copy the entire
> > process image before just throwing it away upon exec, I think Unix,
> > which is based around a philosophy of piping between multiple processes,
> > would have abandoned fork a long time ago. Then again, there is vfork,
> > so I guess they almost did abandon it at one point.
> >
> [...]
>
> vfork is only (!!!) for a fork-exec combination.
>
> So, be aware: do not use vfork, if you don't exec right after it!
>
>
> Ciao,
> Oliver
>
>
>
>
> ---------- Forwarded message ----------
> From: Oliver Bandel <oliver@first.in-berlin.de>
> To: caml-list@inria.fr
> Date: Wed, 6 Jun 2007 11:31:25 +0200
> Subject: Re: [Caml-list] JoCaml Released.
> On Wed, Jun 06, 2007 at 11:22:42AM +0200, Francisco Jos? Valverde Albacete
> wrote:
> > Come on! This is an open forum to learn... You just don't put in an idea
> > only *not to explain it*.
>
> Well, why is the default of this list, that Replies go to private mail
> account?!
> And I got only one person sending an interested reply....
>
> >
> > Please explain what your suggestion was.
>
> OK.
>
> I will try my best.... it follows today.
>
> Ciao,
> Oliver
>
>
>
>
> ---------- Forwarded message ----------
> From: Jon Harrop <jon@ffconsultancy.com>
> To: caml-list@inria.fr
> Date: Wed, 6 Jun 2007 10:40:57 +0100
> Subject: Re: [Caml-list] JoCaml Released.
> On Wednesday 06 June 2007 10:00:38 Oliver Bandel wrote:
> > ...I will collect both mails and send it to the list today...
>
> On Wednesday 06 June 2007 10:00:38 Oliver Bandel wrote:
> > ...is it interests other people...
>
> On Wednesday 06 June 2007 10:31:25 Oliver Bandel wrote:
> > ...I will try my best.... it follows today...
>
> The suspense is killing. ;-)
>
> --
> Dr Jon D Harrop, Flying Frog Consultancy Ltd.
> OCaml for Scientists
> http://www.ffconsultancy.com/products/ocaml_for_scientists/?e
>
>
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>
--
L.G. Meredith
Managing Partner
Biosimilarity LLC
505 N 72nd St
Seattle, WA 98103
+1 206.650.3740
http://biosimilarity.blogspot.com
[-- Attachment #2: Type: text/html, Size: 18821 bytes --]
^ permalink raw reply [flat|nested] only message in thread