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

If anyone has more questions, stoop and I can be found in #AutoNomic on freenode.net... Please feel encouraged to join and discuss this new classic tau project. 

By request, some of my "best of stoopkid" for the past 24h...:




(The above is a quickly thrown together coq proof that LEM holds for all propositions.  The astute reader should also try the proof of the negation.)

I had written up a response pretty quickly, but none of us were particularly thrilled with the tone or the length.  We deliberated for a while (mostly stoop and I) as to if and how to better structure it, and as to if we should even continue to engage this thread at all.

Here is where we've ended up.

Note: this reply includes comments from both myself and stoopkid.  I'll clearly distinguish stoop's responses from my own.  (He has reviewed this post, and given his nod of approval to its' content.)


Not at all, and I stand by my statement.  If agda/coq/idris et al had the particular properties that you claim they do then there would be cases where you could trivially send them off into an infinite loop in type-check/termination-check.  Developers in these languages would often be left wondering if their compiler was ever going to finish, or if it was stuck.  This would not be very practical, indeed.  Luckily, this  is nonsense and simply isn't the case, as they all employ decidable, impredicative, intensional type theory.  (Ofc there are also ITT TFPL systems which allow predicativity/extensionality (or even arbitrary rewrite) and are thus undecidable (even under a most conservative approximate) such as NuPRL or MetaMath's ITT.)

If you have an example of a known-terminating program which does loop the MLTT TFPL typecheck, despite termination check, as you describe (without using "type providers" or similar, anyway) then you should probably report it to the language developers as a bug, I'm sure they'd like to hear about it.  (Such bugs *do* get reported from time to time. For example the only currently known case in agda looks to be https://github.com/agda/agda/issues/1270 but these are *bugs* and treated as such, just as an inconsistency would be, meaning they are always rectified in the implementations.  To date no-one has broken the MLTT TFPL *theory* itself, thus rendering all implementations "loopable.")

(I'm still not entirely sure what it is that you're "missing" here about practicality of MLTT TFPL, but the best I can *suspect* is that it might be the fact that predicates can be internally proven decidable, and one can work solely in such decidable predicates when reasoning about any known terminating algorithm.)


I've asked you many times for any example of any proven-terminating algorithm which cannot possibly be expressed and checked as such in agda/coq/etc.  You've been unable to produce one as of yet.  Until you can, I have to consider your claim of "of course not always" as nonsense.


More nonsense.  Nearly every "major" theorem prover in practical use today (Mizar being the notable exception, but then again it is arguably inconsistent by design) is based on dependent types, ITT, and MLTT specifically.  Outside of academic study, MSOL is, afaik, currently applied only in a few cases of bounded model checking, and virtually always in a hybrid solver.  (Meaning it is almost never used "alone" for general verification, as it would be of too little practical value.  Every solver I'm familiar with which uses MSO combines it with at *least* an SMT solver for integer arith.)

Further, nearly every contemporary type system being developed or added to existing languages for practical use is based on dependent refinements.  I don't see anyone adding MSO type systems to Scala or Rust, or working to build an "MSO Haskell" or "MSO Ocaml" or "MSO Java/C#"....  Are you aware of some such efforts that I'm not finding?  (There are such contemporary efforts to add dependent types to basically every popular language...)


Nonsense.  The only way that this could happen is by a context choosing to adopt an unsound postulate, which would be akin to a context intentionally adopting rules for "stalling" their own chain, or going mao, or...  Yes, there are a lot of ways that a context can *choose* to harm/destroy itself.  This will remain true regardless of the logic employed.  It is not a sensible argument against MLTT for tau.


Epic nonsense.  A postulate is NOT a restructuring of a proof, it is an intentional, partial omission of one.  Further, a postulate may assert anything at all, even a direct inconsistency.  There is, of course, no proof which can not be immediately closed by assuming a postulate.


Partly nonsense.  HoTT/univalence does give decidable function extensionality in MLTT.  However, this is beside the point entirely as postulates (and other inference-affecting annotations) are not a "restructuring" of a proof at all, they cannot affect the behavior of a program - only its typecheck.  (In other words, extensionality has nothing to do with it.)  They can explicitly *omit* some behavior of a program, but generally do not need to as they can be erasable.



Nonsense upon nonsense.  Such an expression restriction is precisely what agda/idris/coq/etc do, and they are entirely decidable TFPLs, that remain computationally complete.  Totality is not undecidable, in fact it is trivial.  (It is also syntactic, just "case alignment," but that is little to do with anything here.)  I think you must be confusing totality and termination/productivity here.  What they "punt" on is a case of termination/productivity check, not of totality.  Productivity check is undecidable in general.  However, by restricting the syntax to reject recursive predicates which can not be asserted terminating/productive by size-change termination arguments, it is kept decidable.  (Again, exactly what Agda/idris/coq/etc do.  For the specific termination check used in Agda, for example, see Abel's "A Predicative Analysis of Structural Recursion."  For an even more formal (and also somewhat more efficient, P-Space complete) treatment, which agda may or may not end up switching to, see Hyvernat's "The size-change termination principle for constructor based languages.")

Does this lead to any syntactic case pattern which must be rejected?  Yes: for example in agda the mutual co-recursion as described on their wiki, as we've discussed at length.  Does this mean they are not computationally complete, or that there are terminating algorithms which cannot be expressed and reasoned as terminating?  No!  Maybe you think that there is some terminating algorithm which cannot possibly be written without these particular "SCT-less" recursion patterns but, again, you have not been able to demonstrate one as asked.  (It seems to me that any such case could just be "loop unrolled" to remove the mutual recursion, since it is known terminating.....)

Even if you could possibly provide such an example, the given algorithm could still be made to be accepted in typecheck by way of a postulate assumption or explicit annotation.  (Or, similarly, if the termination were simply unknown, or "prohibitively difficult to prove," as might the case of your non-example "Collatz example.")


I didn't?  It sure seems like I did...  All well, agree to disagree, or whatever.  Let's move on.


I'm not so sure why this would be (as tau would need all proofs to be bounded to some "reasonable" size constraint, anyway... for practical purposes there is little difference between an infinite derivation and one that takes 1000 years to evaluate on contemporary hardware) but it is a moot point unless you can demonstrate a practical decidability problem by showing a case where the MLTT TFPL typecheck would necessarily loop infinitely over a terminating algorithm.  (There aren't any... so I'm guessing I'm likely to be continuing to wait for this for quite some time.)



Most epic nonsense.  I'm also not so sure that you understand what "computational completeness" means.  MLTT is computationally complete, even without an outer loop.  What is recovered by the "infinite blockchain" model is *Turing* completeness.  These are not the same thing, as you should certainly understand by now.  (Otherwise this is just more indication that you are certainly a long way away from being ready to build a tau, with any logic.)

MLTT (w/ or w/out TFPL constraints) is computationally complete - there is no boolean computable function which it cannot express, typecheck, and extract a (necessarily terminating) program for.  Maybe it is the meaning of "computable function" that you are confused about?  These are the boolean functions that "finite turing machines" can compute, in finite time/space resource.  (Finite turing completeness is and always was the goal.)

Your "complete and consistent" MSO is (necessarily) not computationally complete.  It is simply not possible to have a complete, consistent logic which is also computationally complete, as being computationally complete implies being able to express and reason over full arithmetic axioms.  Any logic which is both consistent and computationally complete will necessarily be incomplete.


Double nonsense.  Self-interpretation is not a requirement for computational completeness.  Even if it were, your argument still doesn't stand up as total languages *can* self interpret (contrary to conventional wisdom) as established recently by Brown-Palsberg.  (Why you'd even make this claim is strange, since both Brown-Palsberg's self interpretation and Bauer's self interpreter for System T were discussed several times on the IRC....)

Note from stoopkid: "the conventional proof only says that there can be no total computable universal function for the total computable functions, and that any such universal function must be strictly partial, but that if a rewrite system is strongly normalizing then it necessarily cannot be this universal function, because a strongly normalizing rewrite system is equivalent to some total function, not any strictly partial function, and thus can't be a universal function for the total computable numbers, so the conventional diagonalization proof doesnt say anything about the expressibility of the total functions defining strongly normalizing rewrite systems in regards to whether or not they can be their own universal function which corresponds to not saying anything about the existence of self-interpreters in strongly normalizing rewrite systems."



Nonsense.  MSO is strictly weaker, as it is entirely and directly expressible in MLTT.  Anything that can be expressed and proven in MSO can be expressed and proven in MLTT.  The reverse is not the case.  To call MSO "more general" exhibits a misunderstanding of *both* MSO and MLTT, and even of logic and the computable hierarchy in general.


Perhaps the reason you never "saw" could be because you drove all of your "team" into another channel, where we continue discussion without you...


Great, so go get to it.... it has actually been many (>6) months, now, since you originally decided MLTT isn't the way, and we haven't seen even the beginnings of an explanation of your design of an alternative. (Or any other new work on your part, since, for that matter...)


I'm not sure how this would be considered "groundbreaking."  It is quite straightforward to see that a block is defined as a product of hashes....


Silly nonsense.  (Sometimes I wonder if you even read the papers that you link.)  Linear inequality of multiplication against a *constant* value does not make for a theory of multiplication.  It is an extension of addition.  (Multiplication by a constant is, of course, just iterated addition.)  Further, the logic employed to establish this limited multiplication in that paper is not even MSO but is "monotone AC-TA."  This adds to my perpetual suspicion that when you say "MSO" you don't really mean "MSO" but "something else..."  Some "other" logic that you have in your head, but can't yet seem to name, describe, or even assert the actual existence of.

Of course it would be self-contradictory for you to claim that multiplication is possible in your hypothetical complete & consistent "somehow MSO-like but not really MSO" logic.  As you rightly elaborate in your blog post, this would contradict Godel.  If tau is to be built with a complete and consistent logic, then it will necessarily omit some portion of basic arithmetic - meaning there will be some math which it *cannot* do in its rules - meaning there will be some routing/topology rules which it *cannot* employ - meaning it will *not* meet the original goal of a fully general, decentralized network.  (This is inescapable without accepting an incomplete logic.)


If you don't know what a general product is, (and why GADTs are important for programming in a typed functional setting) or the difference between a product type and an intersection type, then you are certainly still a *long* way (another year or two, maybe?) from being ready to build a tau, using *any* logic.

Note from stoop: "you might explain why exactly MSO prevents the definability of the general product, even without appeal to godel; mso rules out quantification over functions of arity greater than 1, but the product of two types A and B is equivalent to the polymorphic type Pi C:* . (A -> B -> C) -> C which explicitly requires quantification over that binary relation in order to form it, and since this is just an almost trivial example of a GADT it's got no chance there. btw i'm curious if parametricity results can prove that you need quantification over a binary function in order to express the general product."

(I won't bother explaining this more than he already did, as any further detail can be readily googled up.)



I never claimed that there is only one way to implement a blockchain.  I do claim that any way to build a functional, self-defining blockchain seems to require GADTs.  (Do you have a way to define a block validity function that does not have a domain of block headers which are products of hashes?  I'd be very interested to see that!  *That* would be "groundbreaking." )


So the computational model of Agda doesn't actually exist, and the native compiler is just smoke-and-mirrors?  The hole-filling term inference of Agda and its nice emacs interface are also an illusion?  These tools, which are so easy and approachable that they've been compared to the interface of video games (quite an accomplishment for such a complex software) are somehow actually much less usable than they seem?  Nonsense, nonsense, and nonsense.


Let's just ignore the fact that MSO predated MLTT by quite a bit, and is certainly well set in "the old ways" of the days of Frege and Quine...

MLTT was invented for a "good reason" too: specifically to establish a computationally complete, yet consistent logic.


Personally I'll take a need to explicate types over a lack of general arithmetic/computation any day.


Someone should really let the agda/coq devs know... XD  I don't think that they're aware that they've been doing the impossible this whole time...


Sure, but this doesn't change the fact that this case of (semi/un/partial)-decidability is irrelevant, as it is an offline, user-interactive process and not a part of the network consensus process.


OK, so now I have two examples to request of you!  Can you give an example of a hole in a known-terminating program specification which cannot be filled in finite interactivity steps by the agda hole-filler?

Until you can demonstrate an example fitting this claim, I have to assume that it is nonsense as well.


Again, I guess we'll just have to agree to disagree on this one.  As I see it, any question of what is "simpler" or "more intuitive" is necessarily subjective, but we seem to have a difference of opinion on that.

I, personally, see MLTT as "simpler" because it is like the "yodawg of lambdas."  If you understand lambda calculus then you already understand everything about MLTT except cumulativity.  It's the very same abstraction/application, just done at a type level language instead of the term/object language of the program itself.  It puts the same beta/eta applicative reduction in the type theory as is in the object language.

If you can grok lisp/scheme then you can grok MLTT.  In fact, you basically already know it modulo the impredicative universe hierarchy.

With your hypothetical MSO/TA higher-order model framework it seems that one needs to learn not only the lambda calculus, but also FOPL, some general monadic logic, some set theory, some TA theory, some iterative TA theory, some graph theory, and you'd better know some modular congruence properties and Courcelle theoreom and Seese if you want to do any application at all, and Kobayashi and Ong if you want to do any contemporary, practical application at all... and then odds are where you end up at after all that study you still probably aren't equipped to know how to assert anything but the most basic correctness and reachability properties.... if that.

While I understand that the MSO logics might seem simpler at first glance, and might "sell better," by being just a classical logic, the reality of pragmatic application to "programming in the large" is very much a different story.

You've been studying these logics for ~6 months now, yourself?  Can you show some of the proofs that you've written with them so that we can get an idea of your own level of sophistication in actually using the logics after this dedicated study?  (Are you prepared, yet, to give even a simple proof or still "learning it" to get to that point, yourself?)

Note from Stoop: "he's been studying these systems 6 months and isn't proving anything in them, you should point out that we're now routinely building formalized propositions and verified programs and doing things like proofs of the uncountability of the reals and playing with GADTs and all kinds of other fun things that MSO can't even do, and that tau will come pretty much right away with general computability theory & theoretical comp sci libraries, and related results formalized and ready to work interoperably to aid in chain development, and that we're actually at the point of seriously examining how to actually put together a nomic block-chain in this system." ...  "you might also note that everybody on our team probably has a better understanding of MSO than he does at this point. since we understand it completely fully as just a specific and not very expressive subset of MLTT. and are seeing a more complete picture that illuminates exactly why MSO has the specific properties it does and how those actually relate to the rest of MLTT."

In my experience, most programmers (even "low/entry level") can pick up the basics of MLTT to the point where they can prove over simple-but-useful programs in under a week of dedicated study.  If they're experienced with functional languages (like lisp/scheme) beforehand it is usually more along the lines of 1-2 days of tinkering.  If they're familiar with pure, statically typed functional languages (like haskell/ocaml) it is usually a matter of hours.


Nonsense.  The "vast majority" of real mathematicians/philosophers understand that there are trade-offs, and that they are best served by studying both.  Considering that it is a century-old and still unresolved debate, I don't think you can claim that it can stand as anything but a "matter of taste" in general.  Some mathematicians work in areas where constructivisim is *strictly* necessary, some mathematicians work in areas where classical sets bring ease, and some work in meta-theory where they're required to understand both intimately.  To claim that the "vast majority" reject intuitionism just indicates to me that you haven't spent much time actually talking with many of them.


More nonsense.  I can't even...

Can you show any constructive proposition at all for which it cannot be applied?  (If you can, you've invalidated Glivenko and Brouwer both, no?)

I think what you meant to say was that "not not (p or (not p))" follows in a few steps.  (Again, per Glivenko! (1928))

(Side note: interested on-lookers should be encouraged to read http://plato.stanford.edu/entries/intuitionistic-logic-development/#2.4 for a nice summary explanation of these concepts.)


I am not sure what you find "unintuitive" about it, but again that is a subjective matter.  We'll agree to disagree.

I don't see any case in which it would be "more prone to human errors" however.  After all, we are talking about theorem provers, in which precluding human error is "the whole point."  Could you clarify?


While I agree that in MLTT a statement can not always simply be negated to prove the inverse, this doesn't imply that things are not "either true or false, exclusively" in MLTT.

Of course everything in MLTT is "either true or false, exclusively."  As you just stated yourself, it is consistent.


Our intuition must certainly work differently.  That is OK.  "Agree to disagree" and all.

As to how the "vast majority" of intuitions work, I won't be so arrogant as to assume.... and I don't think that there's been anything like a census...  Feel free to show some statistics on the matter, however, if you know of such a poll!


Not at all, and I'm not sure why you'd think it would.  Can you give some example or explanation of an "incapability" of MLTT to "ultimately support LEM?"


Nonsense.  So I'll ask for a third demonstration from you, can you give me any true, constructive proposition for which LEM as a lemma does not hold in MLTT?

(Fun facts for the astute reader: Note that such a lemma will have as codomain a disjunct of the proposition P and P->_|_ so for any true proposition "inl" holds and for any false proposition "inr" holds.  Being able to show such an example where a LEM lemma could not be applicable would actually require violating LEM by modifying the logic to be 3-valued, which is what justifies LEM as sound (for either classical axiom or intuitionistic proposition) in the first place!  (Hence the name...)

The reason (I'm drastically paraphrasing) that it can not be taken as axiomatic in MLTT without violating consistency is that it would then also have to apply over the top of the universe hierarchy, which would create an infinite regress and prevent closure.  (The cumulative hierarchy could then have no "top" and you're back in the "type in type" or "kind-inconsistency" situation.) The reason it can be applied over any predicate without violating consistency is that there is syntactically no way to apply it over the largest universe, without also implying a larger universe (which it is not applied over) in doing so.

This has some fascinating implications, the most basic of which is that "(P or (not P)) -> ((not not P) -> P)" is trivially provable constructively, but the inverse "((not not P) -> P) -> (P or (not P))" does not hold in general... (I think that this is probably what Ohad is actually trying to point out wrt his statements on proof by contradiction... but who knows) however if we quantify both sides of the inverse implication we can prove that if for all X "(((not not X) -> X)" holds then this implies that for all X "(X or (not X)))" does as well!   I'll leave these (quite informative!) proofs as an exercise for the reader.)

Also, here is a "haskeller level" proof that LEM is intuitionistically sound that you should have no trouble to follow: http://okmij.org/ftp/Computation/lem.html

They go on to prove the existence of the number 42 by contradiction (strong reductio) and close "We have thus confirmed the old result that LEM is intuitionistically justified for decidable propositions."

... An "old result" indeed.  I'm not sure why you would deny it!


You're not wrong.  (Well, maybe you're wrong about what is/isn't intuitive, but we're agreeing to disagree on that, still.  There's probably no way to establish that definitively, short of a census, anyway.)  MSO could be double-negation-transformed into ITT.  You're especially not wrong that this would be particularly "for-nothing" given that it can also be transformed directly in the positive, as well.

In fact, this is largely the least nonsensical thing that you've said here.

However, you're missing the point entirely!  The double-negation transform wouldn't hold in general if it weren't the case that LEM could always be applied.  (Maybe you should try working those 2 "exercise" proofs in that I just mentioned in ITT if you don't understand this...)



(I'm not sure why it is a "practical advantage" exactly... Can you clarify?)

Sure, the core of your (first) argument is "ITT/MLTT won't work" but you've yet to actually give any demonstration of evidence justifying any of the reasoning behind it.  Instead you just make obviously-misguided claims about agda/coq/idris/etc which can be empirically dismissed by just "trying it at home" in agda/coq/idris/etc.... but you refuse to "try it at home" and then you purport it as justification for MLTT not working for a tau.  There may be no bigger nonsense than speaking the opposite of testable fact.


Nonsense.  There are nomics in haskell, nomics in deontic logic, nomics in Drools rules, nomics in coq (predicative CIC derived from MLTT TFPL!), nomics in LKIF (which is expressible in a fragment of owl which is in turn expressible in MLTT TFPL!), nomics in relational algebra (also expressible in MLTT TFPL!), nomics in M$ Excel (the logic of which is probably expressible in MLTT, why not?)..... all of these are decidable frameworks supporting nomic games.  Again you're simply making statements that are contrary to fact.



You "encountered" this, but can not adequately demonstrate or even explain it?


I'd be willing to bet that a "sound MLTT tau" will emerge before you even finish defining and implementing your still-entirely-hypothetical-but-somehow-"MSO-like" logic for your "better" design. :|


NONSENSE.  I've stated our position quite clearly, and completely.  (Also, now, repeatedly.)


If you feel we are incorrect, please prove it.  (It is all that I or anyone else has ever asked of you)    Implement your MSO tau, and destroy our MLTT tau.  We all wish you nothing but the best of luck in both endeavors, but I currently have nothing but skepticism that you will (or even can) accomplish either.



I think that I'm, personally, just about done with wasting my time in responding to your nonsense.  My post was not in response to your blog post (else you would've seen it some time ago) it was in response to a specific request from your community to clarify the position of your lost "team" as most of your community were not privy to our initial reaction to your nonsense in the IRC.

If you feel it was unprofessional of me to answer your community's request for an explanation of our perspective, then I apologize.  I can refrain from polluting their perception with our reality in the future.


Wut?

My apologies, also, for putting faith in your community's ability to comprehend my "technical words" if they choose to.  I'm also quite sorry that you don't have, as I do, confidence in their abilities to understand (or, at least, learn) what we are talking about.

Stoopkid also asked that I mention that we are actively working on putting together introductory materials to explain "tau classic" from first principles, aimed at those without math/programming experience.

(Anyone who can speak a language has the innate ability to grasp logic, so this is just more of your nonsense.)

if we have in hand an msol formula about programs, then before given a program in hand to test whether it fulfills the formula, the formula is translated into an automaton, which can be exponentially large in the size of the formula. once we have the automaton in hand, the runtime is basically linear with known coefficients given any program to validate. the coefficients are exponentially huge but independent on the input program(=tree) size, and we have an explicit bound for the cost of verifying whether a rule is satisfied or not. 


if the rules of the network are redundant enough (eg use WS1S or produce small automaton), then we know that all future verifications of those rules are tractable. also bear in mind that as time passes and the network gains knowledge, proofs will be easier as they can rely on previous proofs.


this is one case. another case would be, assume one block restricts the next block to meet some certain requirements. then we'd like to indeed accept a block that meet them.


have an ability to require only "simple" enough rules (not code, roughly speaking), yes


i think that automaton size results mentioned can prevent such situation.

Sorry, I was incorrect when I said that Idris/Agra produce false negatives, I should have said that given a statement, the result can be undecidable whether it is valid or not.

Yes, the proof process taking too long is what I was getting at. So, you're talking about restricting the input so that the constructed statement considering the prior state and intput should be able to be determined valid or not within a reasonable period of time, correct?  

I'm trying to understand why restricting the possible input so nodes are able to process them all is better than just allowing the nodes to just reject inputs that can't be processed in a reasonable  time period (or in the case of undecidable languages causes the statement to be undecidable). My guess is that each individual node has their own internal state, which means that a scenario could exist where some nodes view an input as valid, others view it as undecidable, (or undecidable given a reasonable amount of processing time), and if that statement was part of a tau block chain it would cause a fork, which wouldn't be easy to reconcile. Is this the reason, or is it something else?

So then you are attempting to build tau with the following properties:

1. Uses a consistent, decidable logic
2. Has input restrictions that prevent a statement that is too complex from being accepted.
3. Has a prover that can take a statement derived by any input that passes the restriction in 2 and any internal state, and test for validity in a reasonable period of time.

Is this correct?

If so, then I'm curious about 3. Is it possible to prove that a prover can do this? If not, won't it be possible for Tau one day to be vulnerable to inputs that pass its restrictions but when combined with the internal state of a node still cause the prover to take too long?

if you speak about the proof process taking too long, then it's not false negative, it's simply undetermined whether the statement was proved or not. moreover, the rules' structure (e.g. the highest order of functions) determine the complexity class and some more parameters of the runtime complexity, so the system can restrict hard problems in desired cases. for example, the logic WS1S (aka MSO over words) is highly expressive, yet is a very narrow fraction of MSO over trees, but the complexity of proof is much more relaxed there. can see about WS1S and WS2S (aka regular trees, or MSO over trees before Ong 2006) in the MONA programming language manual, is a very good document

i dont understand your example. please explain

yes, in consistent system such as idris/agda, once you have proof for something, then it's true. but if you don't have a proof, it doesn't mean it's false, under undecidable system

i cant see why msol would have a false negative problem?

Yes, but if a malicious actor attempts to add a rule to the system which, within the context of the system, can only be determined valid after an inordinate period of time, wouldn't this be a problem for a MSOL based Tau? It would be, for all intents and purposes, be undecidable, correct?

An undecidable system, such as Idris/Agra has false negatives (a valid program is not accepted), but not false positives (an invalid program is accepted), correct?

So, both systems, for all intents and purposes, have a false negative problem. When using Idris/Agra and the user inputs a program that is undecidable, the user is just asked to clarify. Similarly, it would seem, if after a certain period of processing, validity can't be determined by MSOL based Tau, then it would also need to ask the user to clarify, or reject the rule outright.

the proofs being automatic comes from the theory being decidable, and the manual requirements in idris/agda stem exactly from the undecidability problem. and indeed tau must be decidable as it must be a sound nomic game: the network should know when someone obey or break a rule, with no false positives or false negatives. under idris/agda, due to the undecidability, you can obey the rules yet not necessarily be able to prove it.


msol is substantially better as it is decidable (which also imples automatic proofs).


complexity of proof is pretty much the same in both systems (i.e. unlimited complexity). it doesn't mean that even easy tasks will take very long time, it only means that it's able to solve even very hard problems. in addition, k-exptime for example is just a worst case bound. it is commonly said (e.g. by Ong) that this worst case should be achieved quite rarely, and not in common human programs.

I don't know if I'm talking to anybody at this point, but the discussion with HMC and Ohad brings up the following questions:

1. Ohad seems to think that all proofs must be automatic for Tau to prevent malicious actors from attacking Tau. Couldn't the rules of the P2P nodes just require a proof of certain properties to be handed along with the rules for them to be acceptable? Be solvable in a certain amount of cycles using a given Resoner?

A general proof system that can solve all proofs automatically and quickly seems like a tall order. I mean without including the whole distributed computing P2P part of it, such a system would seem to be a major advance over what we have currently with Idris, coq and others.

Yes, the alternatives described would also work with a Turing-complete language, as well, but so what if it did? If using MLTT or MSOL isn't substantially better than a Turing-complete language, then a Turing complete language should be used.

2. Just because MSOL can be solved automatically, this doesn't mean it can be done quickly enough to be useful in Tau, isn't it? I mean that if it takes an exponential amount of time to automatically solve a question proposed in MSOL (and it seems from what I'm read that it is N-EXPTIME), then it might as well be true that some expressions aren't solvable in MSOL, right? And if that is the case, you have the very same problems of MLTT.

Hey All!!

Agoras has been added on C-CEX for voting. This is our chance to add more liquidity and spread the word further.

Please vote for Agoras to be added to C-CEX here: https://c-cex.com/?id=vote&coin=args

 

The problem is whoever is wrong admitting that they are. It can be awkward, even for the person who is correct. I think the best thing would be for Ohad to find people who agree with him to help him finish. I just wish I was more knowledgeable to understand the issues at a deep level.

Hear hear, they're both dedicated to the project so it doesn't matter, they will make it work regardless of who's right or wrong currently.

It's some pretty advance stuff, so we can only speculate. The discussion seems to revolve around theories. So I guess the best thing to do is to implement and see how things work out.

I think they're both protecting their ego. They are probably flaws in both ideas.

Unfortunately I can't tell who's right or wrong in this.

@HMC, any further thoughts from you?

you mix decidability with consistency. of course there is a "problem" with agda/idris when the programmer tries to prove his code's correctness (even if it's correct indeed). the process is not always automatic, and must reject correct code sometimes, which is a clear situation of undecidability. once the programmer managed to convince the typechecker and got proof of correctness, then the proof can be trusted, but that's the situation even with programs in turing complete languages. dependent types simply let one express the requirements from the code in a great generality. proving correctness is another task that sometimes can be done without the language being decidable, but of course not always. there are many ways to verify programs, and dependent types is only one method used in real world applications, but tau needs the decidable and automatic one. indeed the literature on model checking mention those concerns (and more) regarding dependent types, and the state of the art of higher order model checking is msol based, which is possible only since Ong 2006's discovery. simply google "higher order model checking" and see why people are not satisfied from dependent types (hint: mainly due to undecidability but also from being quite complex) and the mainstream is focused on modern methods (hint: msol).


the "few" cases (which are in fact infinitely many) might be enough for malicious players to harm or fool the network by making it unsound and unfair. decidability is needed exactly because not all people say clear truth all the time. but again such restructure (the postulates) is not always possible, and of course is not automatic, and is undecidable problem to show that restructuring maintains the original behavior (as functional extensionality is undecidable on mltt+tfpl). one cannot maintain a huge database of truth if it requires manual intervention (that is not even promised to always work). but now im just repeating ideas i detailed in the blogpost (which you happily ignored).


if i restrict "expressible" to "not all expressibles", then sure..
"expressible" is about syntax. not every well-typed statement well-formed in agda/idris would pass typecheck. being "total" is not part of the syntax, for example. deciding which program is total and which isn't is of course an unsolvable problem in general. MLTT is undecidable, and restricting it to TFPL would be another undecidable task (as i explained in the blogpost).


you answered nothing regarding the problems i mentioned on the blogpost about MLTT or MLTT+TFPL. both being undecidable raise exactly the same concern with Turing complete languages. the fact that it can verify many programs doesn't make it tau adequate, or even smart-contracts adequate.


tau is required to be decidable. maximum expressiveness is a bonus and can't come at the expense of decidability. just like usability cannot come at the expense of security. that's what tau is really about, and for good reasons. this, even though msol over lambdas does not restrict expressiveness more than mltt+tfpl if assuming infinite blockchain, as you assume in your claim that mltt+tfpl is computationally complete.


MLTT+TFPL is not computationally complete. no total language is computationally complete, as it can never interpret itself. even tau classic design requires a turing complete intervention between blocks. modern tau on the other hand is even able to interpret itself, and the language is not total, and is not even normalizing (though normalization can be expressed and decided), therefore in some aspects is way more generalized than mltt+tfpl (not strict generalization ofc), yet it is decidable.


indeed finding the right thing to do is important, yet can never justify doing the wrong thing.


aside ignoring the rest of the paragraph on that blogpost where i mention a way more expressive msol (as a little example, regular trees can express all context free deritvion trees, while even second order recursion trees are context sensitive), i never saw even a small trial of you to reach it. in fact i never saw you studying msol seriously. "there is no msol design for X" means that design should be done. you can't expect modern theories to be as developed as obsolete theories. simply stating "it's impossible" is not my way of work. especially when the original solution (mltt) turns out to be inadequate. with turing complete cycles between blocks (as in the classic design), every logic is nomic-adequate, not securely though without decidability. moreover, even the old and weak regular trees turn turing complete under iteration as mentioned in the tata book, just like your claim regarding mltt tfpl.


that'd be a groundbreaking result. can you prove it?


haha no. in fact even the so-restricted regular trees can do quite much of arithmetic with add and mul, as can be seen here https://staff.aist.go.jp/hitoshi.ohsaki/papers/kobayashi-ohsaki-rta08-fullpaper.pdf


no idea which kind of product you lack here (that say intersection types cannot give), and why you're so convinced there's only one way to implement a blockchain.


well then many of contemporary cs literature can provide you plenty of entertainment, as those three are mentioned in many places. the fact that it can sometimes be done (term inference), doesn't mean it's decidable (i.e. that it's always can be done). and it is undecidable indeed under mltt(+tfpl). in summary, "almost everything" can "almost always" be done in undecidable languages, even turing complete ones. but that's not what tau is about.

the old ways are popular indeed in practice (though i wouldnt say *most* common and popular), but are only the old ways, and now we have new ways that people invented for very good reasons. as a small quote i'll paste from the beginning of http://www-kb.is.s.u-tokyo.ac.jp/~koba/papers/hmc.pdf:

Program verification techniques have been studied extensively, due to the increasing
importance of software reliability. There are still limitations in the current veri-
fication technology, however. Software model checking [Ball et al. 2001; Ball and
Rajamani 2002; Beyer et al. 2007] has been mainly applied to imperative programs
with first-order procedures, and applications to higher-order programs with arbitrary
recursion have been limited. For higher-order programs, type systems have
been recognized as effective techniques for program verification. However, they often
require explicit type annotations (as in dependent type systems), or suffer from
many false alarms. For example, ML type system [Damas and Milner 1982] allows
automated type inference, but rejects many type-safe programs.
This article proposes a novel verification technique for higher-order programs.
The most distinguishing feature of our new technique is that it is sound, complete,
and fully automatic for the class of programs written in the simply-typed λ-calculus
with recursion and finite base types, and for a variety of verification problems,
including reachability (“Does a given program reach a program point fail?”), flow
analysis (“Does a subterm e of a given program evaluate to a value generated at
program point l?”), and resource usage verification (“Does a given program access
resources such as files and memory in a valid manner?”).


just getting from mltt to mltt+tfpl would require a possibly infinite procedure....


all undecidability problems of computation are in general only semi-undecidable, as Hilbert's 10th problem is semi-decidable.


that's simply not true. it can happen some times, but it's impossible for this to happen all the time.


msol is much simpler as it contains much less primitives and decision procedures are fully automatic. claiming otherwise would be either misleading or baffling misunderstanding. is might not be simpler for you but that's only because you're still beginner in msol while somehow experienced with mltt. it's not a matter of taste, mltt (far to mention mltt+tfpl) is way more complex than msol over lambdas, it's just a fact.

vast majority of mathematicians and philosophers find the intuitionistic approach unintuitive. indeed there is a tiny minority of people thinking otherwise, but to picture it like it's a "matter of taste" would be a misrepresentation.


is not an axiom but follows from the axioms in few steps. is in the literature all over....


it is impossible to prove a statement to be both true and false under mltt, as it is consistent indeed, but, proving that a statement is false, doesn't amount as a proof that it's negation is true, in mltt. in classical logic things are either true or false, exclusively. just like human intuition works when it comes to formalism. and just like the vast majority of mathematicians in all eras hold.


sure. and this should give you some clues regarding the incapability of mltt to ultimately support LEM.


no, not "any", otherwise it could be added as an axiom.


the double negation translation shows equi-provability, but my argument regarding LEM was about being intuitive. one could complexify-for-nothing say msol to become intuitionistic via double negation, but one cannot fix mltt to be classic, at least no one yet.


being classic vs intuitionistic logic was only one practical advantage i mentioned of msol vs mltt. it has nothing to do with the core of my arguments.


no decidable logic (including mltt+tfpl) was shown so far, rigorously, to support nomic game. you ask for something that you yourself didn't provide. and it requires work in which for your own reasons you refuse to do. still this is what i work on and i encountered that one cannot have a sound nomic game under mltt+tfpl. you're welcome to move into rigorousity rather handwaving and basis-less claims and present a design of a sound tau based on mltt+tfpl. i dont see how it can be better than a turing complete one.

in summary, you didnt answer to any of the concerns i raised about mltt+tfpl, and you didnt present any reason why msol over lambdas is not good enough for tau. your reply contained so many blatant and subtle mistakes, so apologies if i didn't cover them all on this reply. you're welcome to give a much more professional response to the blogpost. don't expect people to accept any statement that contains technical words.

yes indeed
 

 
In fact people who can realize such goal as the tau, theorized what it will take to build it, have the skills to develop the concrete blocks of building (mathematics and language) and the power to actualy build it, are even fewer. People like that lead, not work on such project. they actualy live that project, it is the one thing that matters for them more than anything else.They can not and will not give up their each personal convictions once they reach it unless proven to be wrong.

Now realize that any given proof about proper logic will be a mathematical proof only, unless build using it.

This is like the difference between a mathematical theory and a physics theory. In physics we say that a theory can only be proven by observation. So is in computers in some way. theory will be proven by it working! But unlike in physicists, rather than being a passive observer, the developer is an active creator. Ohad and HMC practicaly are building the universe in which we all going to live in And no one can do such and be trusted to do that for us unless will be entirely convinced that they are taking the best possible root to create that. It is not a matter of ego in the sense of pride, it is ego in the sense of the truth. The truth that for each and one of us is unique, The truth that make us individuals. Yet life found a way to make all these individual truths to agree on many partial truths in order to communicate and cooperate. Ohad and HMC are now trying to recreate that magic of decentralized cooperation. and they can only do it by being individuals in their believes while communicating and being public about their action. which both are.

They both are taking us on that path to create the tau which we all are allready an important part of it. We are now after the most devastating part of the development in which they each realize and crystallized their theoretical disagreements to the point of having to work on two different routs. yet eventually it will be clear to all which of the two will be the best manifestation of that common idea they share about the tau itself. and their vision of one stable rootchain  will be realized too.  

+100

The above statement (the one above this) was very sad to read, clearly there are very few, very few people in this world, who have the ability to work on a project like this and to see a skilled team walk away, because the Dev seems to have a "my way or the highway" attitude, really sucks.

One man can not complete this project.