W3C home > Mailing lists > Public > www-archive@w3.org > January 2004

subst in n3

From: Tim Berners-Lee <timbl@w3.org>
Date: Thu, 8 Jan 2004 15:10:51 -0500
Message-Id: <C1CB3AA6-4216-11D8-B8A2-000A9580D8C0@w3.org>
Cc: Dan Connolly <connolly@w3.org>
To: Public W3C <www-archive@w3.org>

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
timbl	2. Define the param paters for subst, substN etc -- arbitrary 
choice
Received on Thursday, 8 January 2004 15:10:53 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Wednesday, 7 November 2012 14:17:39 GMT