Quote from: redfish64 on October 04, 2016, 08:08:26 AM

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?

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.

Quote from: redfish64 on October 04, 2016, 08:08:26 AM

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).

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.

Quote from: redfish64 on October 04, 2016, 08:08:26 AM

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?

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.

Quote from: redfish64 on October 04, 2016, 08:08:26 AM

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.

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

Quote from: redfish64 on October 04, 2016, 08:08:26 AM

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?

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