Subject: [icnrg] The logic of CCNx and NDN

From: [email-masked]
Date: Mon, 29 Sep 2014 01:28:47 +0200 (CEST)

Dear all (who attended the Paris interim meeting),

At the risk of proving Kevin right that at the end there will be a 
formal method RG for ICN, it seemed inevitable that I eat my own dog 
food, and do term rewriting.

So here we go: I started capturing the logic of CCNx and NDN, expressed 
in Prolog. Prolog is well suited because it was built for rewriting 
trees (and TLV packets are trees, too).

This use of Prolog has nothing to do with the discussion to consider 
Prolog as a query language instead of Lambda-Calculus.

You can find a first boilerplate at
   http://www.named-function.net/ndnccn-logic.pro

Currently still very compact, it lacks important elements like PIT and 
CS processing. But hey, these are things you can already do:

For example generate all possible data packets that, because of timing, 
might be valid responses (see demo2). Note also from the examples that 
CCNx as well as NDN packets are supported (selectors still to come). 
Ultimately, I would like to investigate the correctness of NDN-over-CCNx 
and CCNx-over-NDN solutions.

I can't dig into this much more right now. Please let me know if 
somebody plans to continue and if you know about similar work.

best, christian

---

/* consumer .       . nodeR1
  *           \     /
  *           f0 - f1 - f2 - nodeR2
*/

fib(f0, [a,b], f1).
fib(f1, [a,b], f2).
fib(f1, [a,b], nodeR1).
fib(f2, [a,b], nodeR2).

repo(nodeR1, [a,b,c], dataForABC).
repo(nodeR1, [a,b,c,d], dataForABCDonR1).
repo(nodeR1, [a,b,c,x], dataForABCX).

repo(nodeR2, [a,b,c,d], dataForABCDonR2).
repo(nodeR2, [a,b,u,y], dataForABUY).
repo(nodeR2, [a,b,u,z], dataForABUZ).

?- demo1([a,b,c]).
Get one document with a name starting with [a,b,c]
      [a,b,c] --> ndnpkt(data([a,b,c,d],dataForABCDonR2))
true.

?- demo2([a,b,c]).
Get all (potential) data objects starting with [a,b,c]
      [a,b,c] --> ccnpkt(content([a,b,c,d],dataForABCDonR2))
      [a,b,c] --> ccnpkt(content([a,b,c],dataForABC))
      [a,b,c] --> ccnpkt(content([a,b,c,d],dataForABCDonR1))
      [a,b,c] --> ccnpkt(content([a,b,c,x],dataForABCX))
true.

?- demo1([a,b,x]).
Get one document with a name starting with [a,b,x]
false.

---
Prof. Dr. Christian F. Tschudin
Uni Basel | Dept of Mathematics and Computer Science
Computer Networks Group | cn.cs.unibas.ch