From: <jos.deroo@agfa.com>

Date: Fri, 8 Sep 2006 01:56:25 +0200

To: hhalpin@ibiblio.org

Cc: connolly@w3.org, Sandro Hawke <sandro@w3.org>, www-archive@w3.org

Message-ID: <OFFBEA3EE1.0E8CE08C-ONC12571E2.008361F1-C12571E2.008377BB@agfa.com>

Date: Fri, 8 Sep 2006 01:56:25 +0200

To: hhalpin@ibiblio.org

Cc: connolly@w3.org, Sandro Hawke <sandro@w3.org>, www-archive@w3.org

Message-ID: <OFFBEA3EE1.0E8CE08C-ONC12571E2.008361F1-C12571E2.008377BB@agfa.com>

Harry, > Jos, > > jos.deroo@agfa.com wrote > > and while that thesis does seem to cover lots of useful > > ground, I don't see the curry/howard stuff there. > > > > > > That is true; that was a challenge that was left :-) > > > My intuition tells me that some sort of small functional core that used > RDF as a sort of typing system might be they way to go for Web Services > as a lightweight alternative to BPELWS. It's unclear to me if you can > squeeze N3-Proofs into some Curry-Howard isomorphism, but if there is a > formal proof theory and proofs can be simplified, it should in theory be > possible. Proving it is an entire another matter :) and first of course > N3 rules would need to be given a proof theory to underlie and maybe > clarify the work it obviously already does in practice. A similar neutral ground I think could be found with pi-calculus in the sense that it can bridge the "declared knowledge" to "execution environment" gap and we are testcasing that and it again all turns around N3 based proofs. > > ) the > > "Turning proofs into running code" is now more turned into > > generating proofs of the form > > > > [ a r:Proof; > > ... # justification components expressed in reason.n3 > > r:gives { > > ... # a theory expressed as a bunch of N3 rules > > }]. > > > > using rule induction i.e. > > > > Given > > Background Knowledge BK > > positive Examples E+ > > negative Examples E- > > such that > > BK does not entail E+ > > BK does not entail E- > > > > then with induction we can find > > Hypothesis H > > such that > > BK and H entails E+ > > BK and H does not entail E- > > > > where > > BK is a set of theories that are not necessarily asserted > > E is any extension set (even the extension of log:implies rules > > in which case the E- are headless rules ie integrity constraints) > > The justification of that H (using reason.n3 ontology) is a closure > > (in the sense that such proof evidence can be reused in further > > abduction plus justification). > > > Quite cool. If you have any URIs that link to code at some point, > throw them my direction! Stay tuned; "the future is longer than the past" :-) At this moment we focus around an implementation like REST /\ || N3 \/ ,------------, | Codd | | /\ | | || Yap | | \/ | | ,--------, | | | Euler5 | | | '--------' | '------------' http://eulersharp.sourceforge.net/2006/02swap/ and a whole bunch of test cases. -- Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/Received on Thursday, 7 September 2006 23:56:41 UTC

*
This archive was generated by hypermail 2.3.1
: Wednesday, 7 January 2015 14:43:03 UTC
*