Topic: Tau-Chain and Agoras Official Thread: Generalized P2P Network - page 154. (Read 309569 times)

I wrote a summary of the current presale status http://www.idni.org/blog/presale-update
Also I updated the description of Agoras http://www.idni.org/agoras

yes

Are you the owner of biggest wallet on bittrex?

Hi Or,
In short and in general, presale is ongoing, still (much) less than 10% were sold, development is ongoing and we're now at the last and hard stage from moving from interpreter to compiler. We're on this stage for quite a while, but we don't want to give up performance, and far to mention - correctness.
Any more specific questions are welcome.

hello Ohad,

What is the current state of the project and the pre-sale?

Just thought I'd check in to thank you folks for the great conversation in this thread. Fascinating stuff. I love this project!

Cheers

Arlyn

Yesterday I gave a talk on a Bitcoin conference in Tel-Aviv, will go up to youtube soon.

I encountered a common question which I'd like to dedicate a post here: do tau really speak about efficient autoproving? Do we have a P-time algo for NPC problems?
Unfortunately, no. Proof is a hard problem, exponential time, no matter which logic we pick, let it be Turing or Martin-Lof or Euclidean geometry.

Yet, tau is not about such uses. It is not about software being able to prove everything automatically. Proof in general is indeed unfeasible. Indeed, we do not expect the autoprover to fully automatically prove that, for example, that any given code meets or not any given requirements, at least not in a lifetime (though theoretically it's always possible with long enough time). Otherwise we could just solve all unsolved math problems.

Nevertheless, the program has to "lead" the prover to the proof, and "miss" only "small enough" details. If you know that your code meets the requirements, you can write it in a way that the prover will find the proof quickly. One cannot expect to write code that depends on very deep insights (like Goldbach conjecture) while hiding it from the prover. At one extreme, code can be as explicit as in Turing machine languages, leaving almost no room for inference. In practice, automatic proving is meant to be used in a way computers can handle, still they're very useful even while proof being a hard task.
Conversely, you can write a proof yourself, or, add some lemmas to make life easier to the autoprover.

The writer of the code should check how many steps it takes to prove the claimed assertions about it, and to keep in mind that users won't use that code if their autoprover is exhausted after some iterations.

Verification of the proof, though, is linear. It is exactly the length of the proof.

The difference between consistent and inconsistent logic is: given a proof, can I trust that the proved statement is true indeed? Under Turing machine logic, both true and false claims can be proved.

VCs typically aren't interested on such type of projects and business models. I think this is obvious, but if you want we can speak more about it.


All presale information is rooted at http://www.idni.org/pre-sale, but I agree that summarizing it in OT is a good idea.


The problem with Turing completeness is that it allows too much - we don't want to add it abilities but rather remove abilities, though in a nontrivial way. For more information please visit the links at tauchain.org that speak about this subject (specifically, "Tau-Chain Primer" and the Let's Talk Bitcoin show).

Fair enough you can add far more to a Turing complete system like user I/o to make it useful. But I think it does behave more like a Turing machine than most computers because presumably in verifying the blockchain you run it in order.

I do not understand Agoras token, why in bittrex sell, start trading. I do not know how many total IPO BTC, it is not already closed, it sent out so many Agoras token, how much money are ready to tau-chain on those tokens become, there is the hands of the team or the community ready to take the number of credits, we do not know, so you start trading, the grass is not too handsome bar.

What about the status of Venture Investment?

I'll keep my reply to this brief(ish) here.  Ultimately this is part of the (much bigger) discussion from the channel about the "implicit vote" aspect of the system.  You are not exactly wrong in anything that you've put, but these are a bit "deeper" details than what Klosure was really looking for, I think.

We generally like to keep the discussion "simple" in our hypothetical scenarios about post-genesis operation, by assuming that consensus proceeds normally by only "on chain mechanics."  You are correct in that such mechanics are not really the totality of the story - it is not actually as simple as "vote per the rules" alone.  There are, of course, actually two additional ways besides "per the rules" that rules can be manipulated!

First, a sufficient number of users simply choosing to diverge their rule selection from that of the rest of the network.  In other words, if a majority of users decide to stray from protocols as decided upon mechanically, and instead follow protocol as decided upon personally, then the network will "follow" the users, despite the new protocol direction being in contradiction with the systematically accepted rules.  This is the scenario that you describe, and it is what we call the "implicit vote" mechanism.  Technically this same mechanism exists, verbatim, in bitcoin.  If suddenly a majority of users decided to block the addresses of a dominant miner, it wouldn't matter how much hash-rate that miner ramped up, they could not continue to produce btc blocks.  This is a form of soft fork.

Second, there is a (quite related) aspect of tau which we refer to as "going mao."  This is where the structuring of the rules (at some context) reaches a point at which the semantics of that context become such that it is no longer the case that all participants in that context are allowed to know (have divulged to them) all rules within the context.  By this mechanism, also, the system can be structured such that rule selection decisions are not longer necessarily entirely "on chain" and per protocol.  This one does not exactly have a direct parallel in bitcoin, except as a loose comparison to a special sort of hard fork.  For tau, this is generally considered something of an "ultimate fail-safe" mechanism for controlling contexts, but is usually seen as something of a "nuclear devastation" option.  It allows for the ability to "revert" a contexts control no matter what scenario has occurred within the rules, but also leaves the knowledgebase of that context (after the event) in a state in which the system can no longer offer all of the same level of assurances to it's users about safety and security of their operation within the network.  This is generally regarded as something of a last resort option for context survival, and the general consensus among our team is that users should generally be quite wary of participating in contexts which have gone this route.

(Of course, as in bitcoin, there is also always the third option of straight up hard forks of the core!  This would also be the only way to change *genesis* rules, and starting from an alternate genesis hash is considered a fork of the core.  However, this is a bit different from what we are really talking about here... which is rule manipulation "on chain.")

However, it is much easier to conceptualize and discuss the basic mechanics of tau without going into the details of these two "context panic button" related aspects, particularly for new people who do not have the same background/exposure to our discussions.  It is generally assumed that these two aspects of the mechanics will only rarely be of concern, and will not be the normal course of operation for tau contexts.  (We might be wrong.  It might turn out, somehow, that users decide that in their post-genesis world it is actually better, for some unknown-to-us-now reason, to leverage the implicit vote and/or changing from nomic to mao as a common matter of course.  I can't possibly imagine that this will be the outcome, as there are  lot of caveats and potential "dangers" to users that arise out of both of these mechanisms, so personally I suspect that these will always be regarded as nothing more than "fail-safes" reserved for only the most extreme circumstances within a context, and will rarely be employed.)


This speaks quite directly to another point that comes up in the IRC from time to time: allocation of resource.  Unlike in btc, where mining is "easy" in that there is only one task to direct all resource toward so mining rigs are basically "set it and forget it," on tau there will always be a decision point when volunteering resources to the network.  The contributor always has to make some choice of "where and how" to apply their contributed resource.  The canonical example is whether to put work toward deepening the root chain with your context pegged, versus work toward deepening your context's chain itself.  Indeed, as you point out, it will be the balance of these trade-offs in resource contribution selections that will keep tau well stabilized and "directed" over time. (At least that is the hope!)

However, I am not sure that I agree entirely with your analysis of how this affects the Agoras token.  Specifically, I don't think there is ever a realistic circumstance (assuming all actors are rational) where the agoras resources could be meaningfully "redirected" as resource contribution back into tau itself in order to influence root rules.  The problem that I see, here, is that if there is some decision point to be made on root, the *original* contributors of the resource into Agoras will divert all of this resource toward operation on root themselves, in hopes of influencing this root chain decision point toward *their* favored outcome, when possible.  This means that such resource will not be available to Agoras users at that time, for them to leverage toward directing root.  In other words, the person providing the resource into Agoras will have to decide if it is ultimately better for them to continue to rent that resource into agoras, effectively "selling" their influence over the rule direction, or if it is better to divert that resource themselves and ensure that any influence it can have is directed in the way that they desire.  I would imagine that for any really meaningful change to tau, itself, at root (which we expect will be an extremely rare event anyway) the decision would almost always be to direct that resource at root themselves instead of continuing to rent.  As such, I'm not sure that it is safe to assume any direct impact from such occurrences on the Agoras token's market value at all.

But then again, I could be entirely wrong on this point.  This is not investment advice, and everyone should do their own considerations of this, and make their own decisions about such a matter!

Trying to speculate heavily, now, on the post-genesis nature of tau is, IMO, likely a fool's errand.  It is very difficult to say what the dynamics will actually end up being in any longer term, and what a post-tau-genesis world will actually begin to look like, beyond simply "different." 

(Woops, that did not end up as being very brief at all...)

I'd just like to jump in and add some more precise and technical detail to Ohad's answer.  I get the impression that you have the background for an appreciation of these details, and you've raised an excellent question that speaks to the very heart of tau's design.

The short answer is that tau provides for both open world reasoning under standard RDF semantics, as well as a fully closed reasoning under an extended type-system.  The tau inference is a staged, cyclical reasoning process that alternates between what we refer to as "open reasoning" (which is OWA and polymorphic) and "closed reasoning" (which is CWA and dependently typed) in rounds, per block of a chain.


Yes, the name is something of a (confusing) joke.  The CWM reasoner employs an open world assumption in general reasoning, as is standard for RDF inference.  It provides this limited facility of scoped negation as failure as a nonstandard extension in it's built-ins.  Unfortunately, as you discovered, this limited ability to reason over a closure often ends up being less than convenient, due to these sorts of interplay with other cwm semantics. (In this case, it's consideration of the whole of the file:// and http:// uri spaces as being subsumed by the kb.)


As Ohad pointed out, we support the slightly more general (but still scoped) negation-as-failure in the style introduced in Eulersharp.  Unlike CWM, this does allow a complement to be calculated all the way up to the background graph, so you can constrain over a whole KB.  (Here tau considers a KB as a parent root context in the typesystem's universe hierarchy, which basically means either the root chain or a sub-context of it.  Tau considers only a specific, finite subset of the uri space as being in the KB scope at any given time, unlike cwm/euler.)


The reasoner is largely functional and already passing much of the cwm/euler swap test suite, but we are still working on testing, debugging, and verification.  We are also currently working on implementing built-ins.  We plan to support most CWM builtin-ins, as well as some of rif, and possibly including some prolog predicates as eulersharp does.  We will also have quite a few tau-specific, of course.


OK, to get down to some real details... what Ohad describes initially in his first example is negation constraint at the most primitive level, scoped negation as failure in the open reasoning representation.  This is, as he points out, generally used to assert a consistency constraint on the KB.  When a reasoning context is assembled, the reasoner first queries to see if "false" can be proved directly, and rejects the kb as inconsistent if it can.

This is a rather *critical* aspect of tau to understand, as it is central to both how tau is able to "reject things" as they are coming in to the system, as well as how it is able to retract or "delete" knowledge that it has previously accepted.  When a new block arrives at a node, potentially containing some new facts/rules, it is run through a series of checks.  The block and it's contents are first speculatively added to the KB, and then the reasoner performs a consistency check.  If the block itself is found to be invalid then it is rejected and ignored, and the speculative addition is rolled back.  If the block itself is consistent, then it's contents are each checked for consistency in turn.  If some rule in the incoming block is contradictory to what is in the KB (meaning some rule addition allows the KB to derive false) then the offending fact/rule that was already existing in the KB is considered deleted (retracted) and is removed from the kb for any subsequent reasoning.

For (a trivial and contrived) example, let's say in block 5 it is asserted (by whatever established means in the existing rules, this is unimportant detail) that { a tau:SuperAdmin; social:likes food:cheese.} asserting that I am a dairy loving user in a special role, and then in block 10 we decide that this special role is no good, and assert the rule {?x a tau:SuperAdmin}=>false.  During processing of block 10, when it is accepted as a valid next block, the conflict between the new rule and the existing fact is discovered.  The source of the conflict from the KB side is traced to the offending fact from block 5, and this fact is removed from the kb.  The fact that I like cheese remains, block 5 is still considered otherwise valid, and the new rule from block 10 is inserted into the kb.  If block 11 tries to re-assert that I am a super admin, it will fail it's initial consistency check, and will not be accepted.  Now if in another block we later come in and introduce a rule of {{?x a tau:SuperAdmin}=>false}=>false we could then re-assert me as a super admin.  (These could even happen both within the same block, as long as the rule was in an earlier transaction in the block than the fact.)

This is a very low level view of our constraint system, however, as it applies "directly" at the "base" RDF open reasoning semantics.  In tau, we additionally define (within the open logic) a more constrained type-system by representing dependent type signatures (to be exact, we will use dependent record types) over top of the rdfs semantics.  Further, we will implement a type-check pass by a set of constraint rules in the open logic that derive false from ill-formed expressions in this type theory.  As such, any KB formed from a context during these "closed" reasoning passes must entirely fit this structuring, and must be total in it's rule definitions.  (Any well formed closed-reasoning expressions are implicitly also well formed in the open RDF semantics, btw.)  By this mechanism, we establish reasoning over a full closure, and "deny" at run-time the open world assumption during this higher level type check.  This allows for the underlying and "open" scoped negation as failure to sit "hidden" under this extended type theory in the form of an uninhabitable Bottom type arising out of the taking of the full closure of a type-checked theory kb.

This still brings us only to a "mid-level" view of complement within the tau design!  Going a step further, we intend to implement over this closed and typed logic (which in turn is implemented over the open and polymorphic logic) the logic of a tractable OWL-DL subset.  (Unlike the closed reasoning logic, which is enforced during any "on chain" reasoning, this OWL layer is an optional extension for the user to choose to employ, or not, at any level.)  This OWL implementation will "hide" the Bottom type of the closed logic in the same way that the closed logic "hides" the SNAF of the underlying open logic.  This allows for a very natural and high level constraint system over acceptable values, cardinality, equivalences, etc for the user without needing much thought on their part about the mechanical details of the complement reasoning that actually occurs at the lower layers.

Whew, that was a lot of information to burn through so quickly!  Long story short, tau will provide any level of closure that you are looking for, with some caveats with regards to network operation and state change over time depending upon which level of closure we are talking about.  (For example, fully open world reasoning cannot also be "authed" on chain...)  Further, don't fear a jump to a consistent OWL-DL ontology too much, as we do intend to support it.

(EDIT: It seems worth noting here that something like OWL-Full is, of course, "right out."  HEH.)

Of course I have only scratched the surface of these details.  I highly suggest checking out some of the reading materials (a couple of them in particular hit directly on these topics) linked from the #zennet IRC channel's topic.  Also, you should feel encouraged to jump into the discussions there, as this will be the best way to learn about these design decisions and implementation details of the system.  Never hesitate to ask us such questions, we actually love re-discussing this stuff.  (It helps to cement our own understanding, as well!)

@HMC
Thanks for the excellent answer, that clears pretty much all my questions so far. I guess next step to understand better Tau is to get familiar with Idris and read Per Martin Lof's Type Theory (BTW for anyone else interested, there is a copy online there. AFAICT this book is out of print, so you will likely not find it in the normal distribution circuit). That's going to keep me busy for a while. I'll come back with more questions once I have digested the underlying theory.

@Ohad
I've been playing a bit with CWM lately, and I'm underwhelmed by how the negation as failure under a closed world assumption is being handled. Unless I've missed something, it seems that the only way to express a negation using basic CWM builtin semantics is to parse a N3 document into a formula with log:semantics and test for the absence of a specific clause in that formula using log:notIncludes. That seems to be confirmed by a few sources: Norman Walsh's blog and some chat he had with Dan Connolly (one of the authors of CWM). These sources are old but CWM hasn't evolved much since and I haven't been able to find any other way by looking at the documentation and test files. If that's still the case, it means that in CWM negation as failure can only be achieved on static documents included in a file and cannot be done on the general context of the reasoner which is always considered to be open world. So much for the so called "Closed World" machine Huh...

Anyway, since your code examples so far have been compatible with CWM, I was wondering how you planned to handle the negation as failure in Tau from a syntactic perspective. If you already have some idea of what the syntax will be, can you please give an example? I'm thinking of a simple case: build a rdf:List of all objects that do NOT have a specific property set. Let's say for instance all objects that are not a fish to continue the example in your (btw very convincing, congrats!) LetsTalkBitcoin interview.

I'm starting to build an application that I will port to Tau as soon as it's functional, and I need a way to express a negation in a closed world. I could move up the food chain to something like OWL and use set semantics to get my way but I'm concerned that this is like going in the wrong direction on the completeness-vs-consistency spectrum and is going to make it more painful to backport the application to Tau in the future. Can you recommand some existing RDF-flavored language that is close to the target in Tau, and that allows to derive negation as failure in a closed world kb without having to rely on static files to do so?

Of the course the ideal would be to start directly with Tau if the reasoner is already functional. But it would also need builtins.. Maybe I can help you with that if you already have a clear idea of what builtins will be available. If you are planning to adopt a subset of the CWM builtins among other things, that could be a good start.

tau can help people make software meet their formal requirements. selecting the requirements themselves is an ethical question already

What is moon in your opinion? Man, I have a hard time understanding even what Bitcoin is capable of. But TauChain, that's a whole different world. If Bitcoin is chinese to an english speaking man, then TauChain is alien language.

It's pretty low, when the beta launches, the price will go to moon.