Re: Cwm/log/n3 rfe: subst

On Mon, 2003-12-08 at 20:56, Dan Connolly wrote:
> Found this while reviewing notes on my WearableGizmo; composed it while 
> jetlagged in Japan diring the TAG meeting...
> 
> ( 'fido 'X {X a Dog}) subst { fido a Dog }.
> 
> C setofall ('X {X a Int. X < 3 }).
> 
> { C setofall (V F) } <=> { this log:forall X. { X a C } <=> (X V 
> F).subst }.
> 
> Hmmm... Would this work for induction?
> --
> Dan Connolly, W3C http://www.w3.org/People/Connolly/


<Zakim> agendum 4. ""Cwm/log/n3 rfe: subst" Mon, 8 Dec 2003 18:56:52
-0800" taken up [from DanCon]
<timbl> ____________________
<timbl> Expose the substitution code as a built-in?
<DanCon> yes...
<DanCon> timbl: setofall seems worth doing in python... ala =
<timbl> Setofall   ?X  such that F(x) is suppoted by G
<DanCon> { C setofall (V F) } <=> { this log:forall X. { X a C } <=> (X
V F).subst }.
<timbl>  M setofall (  `x`   {   ?x   :member W3C }).
<DanCon> my motivation for subst had much to do with figuring out how N3
works; e.g. variables and quoting levels.
<timbl>  M setofall (  `x`   {   foo!log:semantics  log:includes {?x  
:member W3C }}).
<DanCon> motivation came from proof checking, probably.
<DanCon> the list of things that log:includes finds is another RFE that
I'm interested in, independently.
<DanCon> DanC: substitution is a concept that you're allowed to use
without explanation in logic papers
<DanCon> up to simultaneous substituion of N exprs for N vars in F.
<DanCon> (usually called theta, I think)
<DanCon> (and rho)
<timbl> (  "x"   "1".literal       { ?x p o })   subst      { 1 p o
}.     
<timbl> (  "x"   "foo"^uri       { ?x p o })   subst      { <foo> p o
}.     
<timbl> (  "x"   "foo"^uriq       { ?x p o })   subst      { <foo> p o
}.     
<timbl> <foo>  = <bar>
<timbl> (  "x"   "bar"^uri       { ?x p o })   subst      { <foo> p o
}.     
<timbl> NOT (  "x"   <bar>      { ?x p o })   subst      { <foo> p o
}.     
<timbl> hence ^uriq not ^uri
<timbl> Challenges:
<timbl> 1.   Define eth   .literal etc vocabulary once and for all -
arvbitrary chocei

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

Received on Thursday, 8 January 2004 15:15:56 UTC