Pages:
Author

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

sr. member
Activity: 268
Merit: 250
Can the Dev contact.

https://www.coinpayments.net

They are a great storage 2 factor wallet for many coins and tokens.

They accept MaidSafe already and so will have no problem with Agoras.

It is safer in a wallet we can lock much better than on exchanges.


have you tried to use original omni wallet for your agoras? the same was recommended from the beginning.

The advantage for https://www.coinpayments.net

Is it is one wallet for many coins, So Maidsafe, Vox, ETC, and maybe 80 other coins.

If Agoras was listed there it is safe as you can lock your coins and i will not need another wallet and another password etc.
member
Activity: 94
Merit: 10
Sounds like it has all come down to the following:
What if Ohad has come up with something that the Autonomic folks can't even wrap their heads around (at this stage)?  If not, Autonomic it will be.
It's possible; we can only make a comparison based on those aspects of the design that have been publicly disclosed, so we can only really address the question of MSOL vs. MLTT. Both HMC and Ohad claim to know the answers here, but their answers are in contradiction with each other. Previously I had thought I was able to demonstrate the insufficiency of MSOL but upon closer analysis I realized that my proofs were based on flawed assumptions and misinterpretations. Since coming to this realization, have taken a step back from "pushing the MLTT agenda", and now my goal is simply to play the role of a neutral 3rd party and analyze the validity of these claims, along with carrying out some further research into the strengths and weaknesses of various other logical systems that could potentially be used (mainly just standard systems discussed frequently in academic literature on formal logic, as these have the most metatheoretic results available to aid in the comparisons, and are the most likely systems to be brought up as an actual candidate logic as MSOL and MLTT have). I'll share my results with the community as I go along, on the AutoNomic wiki, though I will warn ahead of time that the explanations will still be very technically involved; it's simply a complex subject.

Is it possible that both Tau-Chain and AutoNomic can succeed and work out in different ways with their own merits like PoW and PoS or Ethereum and Tezos may both succeed and work out?
jr. member
Activity: 59
Merit: 10
Can the Dev contact.

https://www.coinpayments.net

They are a great storage 2 factor wallet for many coins and tokens.

They accept MaidSafe already and so will have no problem with Agoras.

It is safer in a wallet we can lock much better than on exchanges.


have you tried to use original omni wallet for your agoras? the same was recommended from the beginning.
§
newbie
Activity: 37
Merit: 0
So basically everyone from "old" tau team  split with ohad and is working on autonomic (the original tau from the videos?) , and ohad is doing his own things now.
newbie
Activity: 35
Merit: 0
Ohad is busy coding away on Tau...Onward
sr. member
Activity: 268
Merit: 250
Can the Dev contact.

https://www.coinpayments.net

They are a great storage 2 factor wallet for many coins and tokens.

They accept MaidSafe already and so will have no problem with Agoras.

It is safer in a wallet we can lock much better than on exchanges.

newbie
Activity: 5
Merit: 0
I have no idea what MLTT or MSOL is... I can only imagine the levels of ego between people with so high level of  proficiency in the field though.  If at some point you guys instead of sticking with the academic literature until your research indicates a flaw in this choice, you will try to unite again and work on it together it will make all the community extremely happy and I am sure will contribute much better to the project.
UNITED WE STRONG
Just MHO

I'm not really sure what you mean wrt "instead of sticking with the academic literature" but I'm willing to work with anybody to either sort out the metatheoretic details or experiment with (open source, publicly disclosed) candidate implementations. The more the merrier. MLTT is simply the candidate the AutoNomic team is currently experimenting with, as it's unfinished business from HMC's original Tau plan. We don't yet have a metatheoretic proof of its insufficiency, so I don't see a reason for us to stop this experiment already in progress. If Ohad wants me to check out his new Tau plans, I'll check them out and give my honest attempt to understand and reach a conclusion, but I kind of guess that AutoNomic is at least one of the reasons that Tau has resorted to non-disclosure.

*shrug*

Me neither. I still find it rather entertaining though. They make seemingly good points but Ohad does a good job defending himself. It's all above my head but I can get a general idea what's going on (I think).

Would someone point my towards the auto nomic thread?

We don't have a thread here, just the freenode channel #AutoNomic.
newbie
Activity: 6
Merit: 0
Quote
Previously I had thought I was able to demonstrate the insufficiency of MSOL but upon closer analysis I realized that my proofs were based on flawed assumptions and misinterpretations.Since coming to this realization, have taken a step back from "pushing the MLTT agenda", and now my goal is simply to play the role of a neutral 3rd party and analyze the validity of these claims
Quote
Adding this question of which logical framework to use has indeed "stalled" at least our side of the project as it's now added the goal of rigorously sorting out the differences between...

I have no idea what MLTT or MSOL is... I can only imagine the levels of ego between people with so high level of  proficiency in the field though.  If at some point you guys instead of sticking with the academic literature until your research indicates a flaw in this choice, you will try to unite again and work on it together it will make all the community extremely happy and I am sure will contribute much better to the project.
UNITED WE STRONG
Just MHO

Me neither. I still find it rather entertaining though. They make seemingly good points but Ohad does a good job defending himself. It's all above my head but I can get a general idea what's going on (I think).

Would someone point my towards the auto nomic thread?
member
Activity: 116
Merit: 10
Quote
Previously I had thought I was able to demonstrate the insufficiency of MSOL but upon closer analysis I realized that my proofs were based on flawed assumptions and misinterpretations.Since coming to this realization, have taken a step back from "pushing the MLTT agenda", and now my goal is simply to play the role of a neutral 3rd party and analyze the validity of these claims
Quote
Adding this question of which logical framework to use has indeed "stalled" at least our side of the project as it's now added the goal of rigorously sorting out the differences between...

I have no idea what MLTT or MSOL is... I can only imagine the levels of ego between people with so high level of  proficiency in the field though.  If at some point you guys instead of sticking with the academic literature until your research indicates a flaw in this choice, you will try to unite again and work on it together it will make all the community extremely happy and I am sure will contribute much better to the project.
UNITED WE STRONG
Just MHO
newbie
Activity: 5
Merit: 0

Sounds like it has all come down to the following:

What if Ohad has come up with something that the Autonomic folks can't even wrap their heads around (at this stage)?  If not, Autonomic it will be.


 Smiley



It's possible; we can only make a comparison based on those aspects of the design that have been publicly disclosed, so we can only really address the question of MSOL vs. MLTT. Both HMC and Ohad claim to know the answers here, but their answers are in contradiction with each other. Previously I had thought I was able to demonstrate the insufficiency of MSOL but upon closer analysis I realized that my proofs were based on flawed assumptions and misinterpretations. Since coming to this realization, have taken a step back from "pushing the MLTT agenda", and now my goal is simply to play the role of a neutral 3rd party and analyze the validity of these claims, along with carrying out some further research into the strengths and weaknesses of various other logical systems that could potentially be used (mainly just standard systems discussed frequently in academic literature on formal logic, as these have the most metatheoretic results available to aid in the comparisons, and are the most likely systems to be brought up as an actual candidate logic as MSOL and MLTT have). I'll share my results with the community as I go along, on the AutoNomic wiki, though I will warn ahead of time that the explanations will still be very technically involved; it's simply a complex subject.

It's very difficult to understand all of this. I guess possibly for 99%+ of us here. What's going on? Who are these people? And these other projects? Anyone care to elaborate? Will this stall the project? Is there a risk of a dead end?

Thanks in advance.

I'm guessing you mean HMC, myself and the AutoNomic project? Anyway, we were all originally working with Ohad but we split for various reasons, one major factor being Ohad's choice to change the planned logical framework from MLTT to MSOL. The history's all in the thread and the IRC logs, and I don't feel like dragging it up. Tau continued as same name, new design. AutoNomic continued as same design, new name. Adding this question of which logical framework to use has indeed "stalled" at least our side of the project as it's now added the goal of rigorously sorting out the differences between... nearly every standard logical framework presented in academic literature on the subject or in modern use in automated theorem proving and proof-checking, though we are still developing the MLTT-based client in parallel to this for concrete experimentation (and because until our research indicates a flaw in this choice we'll continue under the operating assumption that it will still eventually be the chosen framework). I can't speak to what's going on on the Tau side of things though (from what I understand it's not even publicly disclosed).

Edit to fix grammar mistakes.
newbie
Activity: 27
Merit: 0
It's very difficult to understand all of this. I guess possibly for 99%+ of us here. What's going on? Who are these people? And these other projects? Anyone care to elaborate? Will this stall the project? Is there a risk of a dead end?

Thanks in advance.
sr. member
Activity: 434
Merit: 250
I've been asked to address this post directly.

First, a small disclaimer: I post this as a personal response, not as a representative of the Autonomic project.  This post has not been discussed with the others, and does not necessarily reflect the views or official positions of our project.

Quote
As a result three questions / remarks which I found very interesting were left unanswered / undevelopped to my disappointment.

Quote
23:37 < HMC_a> so yes or no, is there a second(+) order expression which cannot be consistently proven in any mso framework?  In general is full second/third order collapsible to msol, or isn't it?

I expect this one must be discussed somewhere in the works of Bruno Courcelle so you could point us to some theorem or conjecture if that can save you some time with the explanations. Don't worry about making it understandable for the mere mortals. I'm happy with an explanation that I can't fully comprehend so long as HMC and you seem to be on the same page.

Of course there are such expressions.  Ohad's refusal to admit this (even contradicting himself by giving both answers) remains baffling to me.

Here is what is commonly considered one of the "canonical" examples, and it is commonly used to prove various meta-theoretical differences of second order logics:
Code:
F(Y) = forall X . (forall x,y,z . (X(x,y) -> X(y,z) -> X(x,z)) -> (forall x:Y . exists y:Y . X(x,y)) -> (exists x:Y . X(x,x))) or all x . not Y(x)

This is the class definition of finite structures.  It has no mso or fol equivalents.  Its' negation is the class definition of infinite structures, and ofc also has no mso/fol equivalents.

We've covered at least one or two dozen such examples in the autonomic channel over the past few months.  Lately we've been discussing the expressibility boundary between full second order and Henkin semantics, as this is particularly relevant to the decidability of logics above first order.  In that context, here is my favorite working example, due to its' amazing simplicity in illustrating:
Code:
forall x,y . exists P . P(x,y)

This is logically valid in full second order semantics, but does not collapse to first order as valid.  Under Henkin sol semantics it is conditionally satisfiable.

Quote
Quote
22:17 < HMC_a> but maybe I'm missing some collapsability magics, somewhere, so perhaps you could give a concrete example of verification of such an example?

I concur wholeheartedly with this one. A simple example of a second or third order program in STLC+Y with limited inputs, executed against all input combinations and encoded as a tree, and then the demonstration of how msol verifies it would be hugely helpful getting some intuitive understanding of how it works. That would give us the tools to try to find a case where it doesn't work (there shouldn't be any). You can recycle that explanation for the whitepaper, so no time wasted here.

Note that his given example does not meet the request.  It is a first order program, with unlimited/unconstrained inputs.  His verification does not assert any property of the IO relation, for any inputs - it only verifies that the function is constant.  (I agree that this property is first order expressible...)  

He also seems to conflate order of functions of a signature with order of logics over a signature.  (He doesn't seem to understand order of functions, either, for that matter...)

(EDIT: It was later pointed out to me that Ohad made a second post with a second example expression which was a higher order function.  It still has unlimited/unconstrained input, asserts no property of IO relation, and he still verifies only a first order property of the output (as he points out at the end of his post) so this is also not an example that meets klosure's request.)

Quote
Quote
22:18 < naturalog> in bohm tree you dont have lambda terms
22:18 < naturalog> they're all reduced already
22:18 < naturalog> so the higher order rules disappear and remain only with true/false or other info

What kind of reduction are you talking about? How can the result not have lambda terms? Do you mean no lambda abstractions / bound variables? How do you guarantee that?

I'm afraid that I can't speak much to this one.  Looks like nonsense to me.

Quote
I understand that you probably don't want to bother making these explanations if you feel the tone of the conversation on IRC was not respectful, but please remember that IRC conversations are more or less supposed to serve as documentation and research log in the absence of actual documentation, and that they benefit the entire community, including investors and potential future devs who can help you on the code, so it would greatly help if technical questions are actually being answered.

You can find significant discussions of these topics in the #autonomic logs.  I'm not following ##idni anymore but am told by others that it has devolved into a weird sort of echo chamber, mostly about (very old) solutions to transform problems and with very little to do with any particular logics.  I'm guessing you would not find any clarifications there.

I'm also told that Ohad has now given up on mso entirely and moved to more expressive logics.  From what I hear it sounds like he is lately exploring the region around/above the P-space logics, and in the "murky" area between the exptime algorithms and primitive recursion.  (It is still unclear to those I've spoken to what the logic he "has in his head" actually is.  AFAIK he still has not done anything to make concrete (or even further describe/qualify) his proposed framework.)

I like to joke that he is slowly making his way up the complexity families, and may even soon rejoin us in exploring "true" omega-order HOLs with full semantics, covering the full arithmetical hierarchy and in the existential N*N fragment of the analytic hierarchy.
(I can only hope that, along the way, he remembers/rediscovers why completeness and deductive proof inference should be considered problems for the system, not features.)

As far as I'm concerned, the debate about "mso v mltt" has become entirely moot.  There still seems to be room for debate wrt: completeness, decidability/term-inference, Lowenheim-Skolem/compactness/Lindstrom, (general) consistency of collapse of expressions between orders, consistency of LEM as axiomatic, or the necessity of general expression within the system.  He still must disagree on one or more of these points, otherwise he'd inevitably have to just be back at MLTT as the only possible option - and back on track with the "oldtau" plan.

If he did "come around" it is unclear to me if our A.N.O.N. project members would welcome him back with open arms or tell him to go jump.

Personally, my position remains that all are welcome.  Unlike newtau lately, we do not generally seek to moderate ideas or hide our design-detail information.

Edit: fixed typos
hero member
Activity: 897
Merit: 1000
http://idni.org
heh answered too fast, will give a 3rd order example right away (will edit here)

EDIT:
take the following third order stlc program (which always returns 2):
\G \H \z. H G z \y.y \S \x. S x 2

which is equiv to the following c++11 program:

#include
#include
using namespace std;
int g(int y) { return y; }
int h(function S, int x) { return S(x); }
int f(function G, function, int)> H, int z) { return H(G, z); }
int main() { cout<< f(g,h,2)<
writing the program as:
@(2,@(x, @(\S\x.S, @(\y.y, @(z, @(G, @(H, \G\H\z))))
the bohm tree would be:
@(2,@(x, @(\, @(\, @(z, @(\, @(\, \(\(\))))))

asserting that the leaf is always labelled 2 is straight forward even in first order logic.
hero member
Activity: 897
Merit: 1000
http://idni.org
thanks,

@Ohad, I have a question. I've skimmed through the IRC logs of the last two months and found a very promising conversation between you, HMC and Stoopkid on 6 June about the maths of the new Tau.

that wasn't about the math of the new tau (as its logic is beyond what mentioned there) but i deliberately didn't want to expose any design detail, so i let the discussion revolve around mso vs mltt. the old vs new tau is already (and was back then 2m ago) light years from that subject

As far as I have been able to understand, HMC and Stoopkid where trying to understand how MSOL is able to verify higher order programs in spite of not being itself a full second order logic.

well they spoke about "higher order logic" without saying what it actually refers to, and this is part of what made the discussions very futile: the order of the logic is only one property of a logic, it by no means tells everything interesting (like expressiveness or decidability) as for itself (but in conjunction with other properties of the logic in concern).
but indeed as you point out, i answered for the scope of verifying higher-order functional programs. and indeed (as below), stlc is higher order (and the Y can make it "infinite order" call it so). so if we got an stlc program we can verify it using mso formulas over its bohm tree (as below).

And you were answering something about the higher order program being fully beta-reduced and encoded as a tree which apparently was supposed to turn it into a first order expression.

a program, on this setting, is something that returns a first order expression, i.e. it reads an input and returns an output being objects, not functions. however the program can still be higher order, calling functions and functions of functions, but at the end return an object. therefore it is of no surprise that the result of the execution (=beta reduction) doesn't end up with a function. however execution has a trace, and all possible traces (wrt all possible inputs) yields a tree, which is the bohm tree.

Then the tone quickly deteriorated, and you ended up rage quitting the conversation without finishing your explanation.

i really didnt see any point in explaining as every word i say is then (intentionally or not) misinterpreted to completely other fields. a good example is the mis-use of the term "higher order".
then i tried to see whether it's a misunderstanding problem or a personality problem, so i moved to speak about being gentleman.

As a result three questions / remarks which I found very interesting were left unanswered / undevelopped to my disappointment.

Quote
23:37 < HMC_a> so yes or no, is there a second(+) order expression which cannot be consistently proven in any mso framework?  In general is full second/third order collapsible to msol, or isn't it?

that's just another mis-usage of the concept of order. as above. can you please explain me the question at the scope of verifying higher order programs? i dont see how the question make any sense. the program need not collapse to its spec (?!)

I expect this one must be discussed somewhere in the works of Bruno Courcelle so you could point us to some theorem or conjecture if that can save you some time with the explanations. Don't worry about making it understandable for the mere mortals. I'm happy with an explanation that I can't fully comprehend so long as HMC and you seem to be on the same page.

courcelle has nothing to do with program verification or stlc+y as far as i know.
he's the mso over graphs guy.

that all said, i'll really very happily explain anything, just please give me a question i can understand and not a paste of hmc's pile of buzzwords.

Quote
22:17 < HMC_a> but maybe I'm missing some collapsability magics, somewhere, so perhaps you could give a concrete example of verification of such an example?

I concur wholeheartedly with this one. A simple example of a second or third order program in STLC+Y with limited inputs, executed against all input combinations and encoded as a tree, and then the demonstration of how msol verifies it would be hugely helpful getting some intuitive understanding of how it works. That would give us the tools to try to find a case where it doesn't work (there shouldn't be any). You can recycle that explanation for the whitepaper, so no time wasted here.

here's a third order stlc program:

\x.\y.\z.x

the bohm tree looks like \x->\y->\z->"x"
i.e. is a list on this case (because we dont use application on this specific program).
now you can write an mso (or even fo) sentence "t is a leaf -> t's label is x" to verify that the program always returns x.

(this question was very specific so no problem answering it)

Quote
22:18 < naturalog> in bohm tree you dont have lambda terms
22:18 < naturalog> they're all reduced already
22:18 < naturalog> so the higher order rules disappear and remain only with true/false or other info

What kind of reduction are you talking about? How can the result not have lambda terms? Do you mean no lambda abstractions / bound variables? How do you guarantee that?

as explained above, a higher order program that returns an object is a first order term, no matter that inside it calls higher order terms. now, because it returns an object, it *must* beta-reduce to an object! after execution, you have no functions left, only data.

and again will gladly explain further.
newbie
Activity: 33
Merit: 0
Has there been any news about the impending Agoras release?
I think I would like to purchase more AGRS tokens if there is a release imminent Smiley
Thanks.

too long before Agoras release
newbie
Activity: 50
Merit: 0
@Ohad, I have a question. I've skimmed through the IRC logs of the last two months and found a very promising conversation between you, HMC and Stoopkid on 6 June about the maths of the new Tau. As far as I have been able to understand, HMC and Stoopkid where trying to understand how MSOL is able to verify higher order programs in spite of not being itself a full second order logic.  And you were answering something about the higher order program being fully beta-reduced and encoded as a tree which apparently was supposed to turn it into a first order expression. Then the tone quickly deteriorated, and you ended up rage quitting the conversation without finishing your explanation.

As a result three questions / remarks which I found very interesting were left unanswered / undevelopped to my disappointment.

Quote
23:37 < HMC_a> so yes or no, is there a second(+) order expression which cannot be consistently proven in any mso framework?  In general is full second/third order collapsible to msol, or isn't it?

I expect this one must be discussed somewhere in the works of Bruno Courcelle so you could point us to some theorem or conjecture if that can save you some time with the explanations. Don't worry about making it understandable for the mere mortals. I'm happy with an explanation that I can't fully comprehend so long as HMC and you seem to be on the same page.

Quote
22:17 < HMC_a> but maybe I'm missing some collapsability magics, somewhere, so perhaps you could give a concrete example of verification of such an example?

I concur wholeheartedly with this one. A simple example of a second or third order program in STLC+Y with limited inputs, executed against all input combinations and encoded as a tree, and then the demonstration of how msol verifies it would be hugely helpful getting some intuitive understanding of how it works. That would give us the tools to try to find a case where it doesn't work (there shouldn't be any). You can recycle that explanation for the whitepaper, so no time wasted here.

Quote
22:18 < naturalog> in bohm tree you dont have lambda terms
22:18 < naturalog> they're all reduced already
22:18 < naturalog> so the higher order rules disappear and remain only with true/false or other info

What kind of reduction are you talking about? How can the result not have lambda terms? Do you mean no lambda abstractions / bound variables? How do you guarantee that?

I understand that you probably don't want to bother making these explanations if you feel the tone of the conversation on IRC was not respectful, but please remember that IRC conversations are more or less supposed to serve as documentation and research log in the absence of actual documentation, and that they benefit the entire community, including investors and potential future devs who can help you on the code, so it would greatly help if technical questions are actually being answered.

I'm really glad to see that you, HMC and Stoopkid are trying to get back to discussing the maths, but at the same time your (as in all three of you) lack of maturity is really appalling. You are reading like an old divorced couple who hate and yet still love one another, pulling each other's leg every few sentences,  and lacing otherwise perfectly factual questions and answers with half concealed vitriol and sarcasm. Rage quitting and yet coming back for more. Really not constructive. A giant waste of time and intelligence.

If you really care as much about Tau / Autonomic as you all pretend, you should be able to keep your egos in check and apply a minimum of self-control to make sure that conversation doesn't turn into a nasty troll fest before it has the time to reach its conclusion. After all, if both of your are confident about your maths, it really shouldn't be a problem to set the record straight. And if you are not, it's fine (who am I to judge?), but then stop acting as if you are Field medalists and be humble and honest about what you don't know.
newbie
Activity: 15
Merit: 0
Has there been any news about the impending Agoras release?
I think I would like to purchase more AGRS tokens if there is a release imminent Smiley
Thanks.
member
Activity: 116
Merit: 10
They speak "chinese" there man Smiley

So true...  lol   Grin



A group of aliens from "Tau" galactic planning the invasion to mother earth... I like it Roll Eyes
they gonna finally fix our poor planet )))))
jr. member
Activity: 59
Merit: 10
Hello there, what is the best/safest way to store IDNI? Thank you in advance.

hey!! try omni wallet like others do. i haven't seen better answer here.
member
Activity: 116
Merit: 10
1º go to https://webchat.freenode.net/ ...
2º in the nick name put any nickname
3º in chanelss, put ##idni
4º connect...


Thanks friend but that's not the problem, I already have my nick and enter the channel ## idni. The problem is that I do not find the thread of what has happened all this time in that channel. Is it all in real time and deleted? Is there a thread to see? Sorry for being such a beginner. But beyond that it is clear that it is not a web site that is suitable for everyone to see easily what is being done. Although your good reason will have Ohad! Thank you.

Yes, I had that feeling as well. IRC is for devs. I also couldn't find the history of chat so just left it open for a day. They speak "chinese" there man Smiley so If the rest of the thread is same, we won't understand clearly what is going on anyways... But at least it gives sence of progress. We need to wait for white paper and official announcements.
Pages:
Jump to: