Re: universal languages

Dan Connolly wrote:
[...]
> Here's what I'm hoping to do with this stuff:

I neglected to mention that I've got a pretty good start
on a lot of this...

>         (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)

ist(context F) looks a lot like says(P F) from the PCA
paper, but I haven't gone beyond the intuion stage there...

>         (b) map the Boomborg-PC syntax to McDermott's RDF-ish syntax
>                 (ugly syntax engineering, but nothing subtle)

Note that McDermott's approach is very close, syntactically,
to the PCA/ELF approach: there's just one variable binder,
and forall and exists are one-argument constructs.

http://lists.w3.org/Archives/Public/www-rdf-logic/2000Dec/0044.html
http://www.cs.yale.edu/homes/dvm/daml/proposal.html

(oh... by the way... another proof checker I've been
working in/on lately:
  http://www.w3.org/2000/10/n3/proofcheck.py
which is a port of McCune's proof checker.)

>         (c) use this in stead of larch to specify
>                 URIs (esp DesignIssues/Model; beyond syntax)

http://www.w3.org/XML/9711theory/URIclient.lsl
$Id: URIclient.lsl,v 1.1 2001/01/31 07:39:53 connolly Exp $

>                 HTTP (esp. stuff like max-age)

http://www.w3.org/XML/9711theory/HTTP.lsl
$Id: HTTP.lsl,v 1.9 2000/01/17 21:33:40 connolly Exp $
(not up-to-date w.r.t. recent thinking on RDF and URIs)

>                 XML (esp. infoset)

I started doing this one a while ago; recently,
I figured the XML query algebra would be more concise;
it turns out that the XML Query data model spec
is almost identical to the XML Infoset spec. Sigh.

http://www.w3.org/XML/9711theory/XMLInfoSet.lsl
$Id: XMLInfoSet.lsl,v 1.5 1999/09/01 06:26:40 connolly Exp $

I'm not sure I'll bother to update this one, given that
the query stuff pretty much replaces it...

>                 XPath (based on my larch translation of Wadler's work)

http://www.w3.org/XML/9711theory/XPathWadler.lsl
$Id: XPathWadler.lsl,v 1.8 2000/01/17 21:33:41 connolly Exp $
(not synchronized with some of this other stuff yet)

>         (d) mix in digital signature

no tangible progress there yet.

>         (e) continue with
>                 XML Schema (give MSL the once-over)

I haven't started with MSL; my larch version of XML Schema
is really out of date
http://www.w3.org/XML/9711theory/XMLSchema.lsl

>                 XML Query (maybe get them to use this
>                         syntax in stead of, or alongside
>                         their functional programming notation?)

http://www.w3.org/XML/9711theory/XMLQueryDataModel.lsl
$Id: XMLQueryDataModel.lsl,v 1.1 2001/01/31 07:39:53 connolly Exp $


>         (f) then do
>                 RDF (rename RDF99:model to McCarthy:abstract-syntax

http://www.w3.org/XML/9711theory/RDFAbSyn.lsl
$Id: RDFAbSyn.lsl,v 1.1 2001/01/31 07:39:53 connolly Exp $

>                         think hard about relative URI references.

see URIclient.lsl above

>                         proof theoretic and model theoretic
>                         specifications for refication.)

groundwork:

http://www.w3.org/XML/9711theory/FormalSystem.lsl
$Id: FormalSystem.lsl,v 1.3 2000/10/31 22:26:31 connolly Exp $

>                 RDFS (answer Peter's question of
>                         can bags contain themselves?)

no tangible progress there.

>                 DAML (transcribe KIF axioms into this notation;
>                         use contexts to specify
>                         DAML:imports)

I wrote a KIF parser in python
  http://www.w3.org/2000/10/n3/KIFSyntax.py
  $Id: KIFSyntax.py,v 1.2 2001/01/27 22:43:59 connolly Exp $
and I think TimBL is using it to convert the KIF
axioms to n3. He's got a converter from n3 to RDF,
but it doesn't handle quoting/reification really, yet.
I think he'll need something like McDermott's proposal
in order to realistically represent this stuff in
anything like RDF.

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
office: tel:+1-913-491-0501
pager: mailto:connolly.pager@w3.org
  (put return phone number in from/subject)

Received on Thursday, 1 February 2001 15:13:12 UTC