Re: universal languages

"Peter F. Patel-Schneider" wrote:
> 
> From: Dan Brickley <danbri@w3.org>
> Subject: Re: universal languages
> Date: Thu, 1 Feb 2001 13:48:52 -0500 (EST)
> 
> > On Thu, 1 Feb 2001, Peter F. Patel-Schneider wrote:
> >
> > > From: "Tim Berners-Lee" <timbl@w3.org>
> > > Subject: Re: DAMl "Thing" should be Top, Universal class - including concrete types
> > > Date: Thu, 1 Feb 2001 13:15:52 -0500
> > >
> > > > We are not designing a reasoner. We are making
> > > > a universal language which will allow the expression of information
> > > > from many [different] systems. When a given system has limited descriptive
> > > > power, then its input and output will be limited to a subset of the
> > > > language.
> > > >
> > > > Tim
> > >
> > >
> > > OK. In line with this comment from Tim, let me put forward a proposal for a
> > > universal web language.
> > >
> > >
> > > Requirements:
> > >
> > > The universal web language (UWL) will be able to directly represent the
> > > meaning of any statement about any state of affairs that may be made by any
> > > application that interacts with the world-wide web.
> > >
> > > Language:
> > >
> > > I propose that Montague logic be used as the UWL.
> > >
> > > Rationale:
> > >
> > > Montague logic was designed to capture the meaning of natural logic
> > > utterances, which should be adequate to represent anything.
> > >
> > >
> > > Any problems with this?
> >
> >
> >
> > Sounds great. Can you point me to any software I can download to do useful
> > things on the Web with UWL...?
> >
> > Dan
> >
> 
> Precisely.

I don't know what Montague logic is, but I'd like to learn.
Sounds interesting.

There are some logics that I think are close to what Tim's
talking about.

As to useful software, how about this?

[[[
4.Mobile agents. In this set of experiments we extend the safety policy
to
     include resource usage bounds and data abstraction, in addition to
     memory safety. In a paper to appear in a special LNCS issue on
     mobile-code security, we describe the use of PCC to ensure the
safety of
     untrusted agents that access a database of airfares. Such agents
are
     assigned an access level when they are received and are required to
look
     only at those database records whose access level is smaller. This
     requirement is not enforced at run-time, but instead it is a part
of the
     proved safety properties. In addition, the agents must prove that
they
     terminate within a given number of instructions, and if they send
network
     packets, they are not exceeding a preset bandwidth. For an example
     agent using this safety policy, the proof is about 6 times the size
of the
     code. 
]]]

--        Proof-Carrying Code
http://www.cs.berkeley.edu/~necula/pcc.html#implementation
Tue, 22 Jun 1999 01:33:41 GMT


The first time Tim and I found something pretty close to what we
want was the PCA paper:

[PCA] Proof-Carrying Authentication. Andrew W. Appel and Edward
      W. Felten, 6th ACM Conference on Computer and Communications
      Security, November 1999. 
http://www.w3.org/DesignIssues/Logic#PCA

the logic in there is based on a logic framework that
looks pretty hairy... one of these typed lambda calculus
thingies. There's a proof-checker in 13130 lines
of C code, with integrated digital signature support, but
the style of C is sorta ML-ish, and I don't really grok.
  http://foxnet.cs.cmu.edu/pcc/oct98.html

But there's lots of related work... proof checkers based
on typed lambda calculus are evidently pretty commonplace.
Just the other day I found one that runs as an emacs mode:

"Boomborg-PC is a proof-checker of Calculus of
Constructions that runs on a buffer of GNU
Emacs. Calculus of Constructions, proposed by Thierry Coquand and Gerard
Huet, is one of the
so-called higher-order typed lambda-calculi."
-- http://nicosia.is.s.u-tokyo.ac.jp/boomborg/boomborg-pc.html

The source code, which includes interactive support in addition
to the actual proof checking stuff, is a few KLOC of elisp:

   3651   13289  115615 pc.el

It requires MULE to display funky characters like lambda
and PI, but once you install that (which is easy
on a debian linux box, by the way) it's a snap to
install and play around with.

Here's what I'm hoping to do with this stuff:

        (a) model Guha's context logic in typed lambda calculus
                (should be an elegant
                front-side-of-one-page sorta thing;
                a few hours work, if it'll work at all;
                ist(context F) looks easy;
                the nonmon stuff (circumscription) scares me though;
		I'll probably skipt that)
        (b) map the Boomborg-PC syntax to McDermott's RDF-ish syntax
                (ugly syntax engineering, but nothing subtle)
        (c) use this in stead of larch to specify
                URIs (esp DesignIssues/Model; beyond syntax)
                HTTP (esp. stuff like max-age)
                XML (esp. infoset)
                XPath (based on my larch translation of Wadler's work)
        (d) mix in digital signature
        (e) continue with
                XML Schema (give MSL the once-over)
                XML Query (maybe get them to use this
                        syntax in stead of, or alongside
                        their functional programming notation?)
        (f) then do
                RDF (rename RDF99:model to McCarthy:abstract-syntax
                        think hard about relative URI references.
                        proof theoretic and model theoretic
                        specifications for refication.)
                RDFS (answer Peter's question of
                        can bags contain themselves?)
                DAML (transcribe KIF axioms into this notation;
                        use contexts to specify
                        DAML:imports)

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/

Received on Thursday, 1 February 2001 14:42:03 UTC