文件列表:

LICENSE (1068, 2021-01-21)
axiomforest/ (0, 2021-01-21)
axiomforest/TruthValue.java (2763, 2021-01-21)
axiomforest/λ.java (9942, 2021-01-21)
axiomforest/λObserver.java (17512, 2021-01-21)
axiomforest_old/ (0, 2021-01-21)
axiomforest_old/observe/ (0, 2021-01-21)
axiomforest_old/observe/Λ.java (5841, 2021-01-21)
axiomforest_old/observe/ΛObserver.java (893, 2021-01-21)
axiomforest_old/observe/λtv.java (653, 2021-01-21)
axiomforest_old/superposition/ (0, 2021-01-21)
axiomforest_old/superposition/λ.java (4497, 2021-01-21)
axiomforest_old/superposition/λObserver.java (4099, 2021-01-21)
axioms/ (0, 2021-01-21)
axioms/WikibinatorV0.java (468, 2021-01-21)
data/ (0, 2021-01-21)
data/wikibinator/ (0, 2021-01-21)
data/wikibinator/exampleCode/ (0, 2021-01-21)
data/wikibinator/exampleCode/exampleCode001 - Copy (2).λ (4720, 2021-01-21)
data/wikibinator/exampleCode/exampleCode001 - Copy (3).λ (6101, 2021-01-21)
data/wikibinator/exampleCode/exampleCode001 - Copy (4).λ (6545, 2021-01-21)
data/wikibinator/exampleCode/exampleCode001 - Copy (5).λ (7494, 2021-01-21)
data/wikibinator/exampleCode/exampleCode001 - Copy (6).λ (7795, 2021-01-21)
data/wikibinator/exampleCode/exampleCode001 - Copy.λ (3352, 2021-01-21)
data/wikibinator/exampleCode/exampleCode002 - Copy (2).λ (8121, 2021-01-21)
data/wikibinator/exampleCode/exampleCode002 - Copy (3).λ (1820, 2021-01-21)
data/wikibinator/exampleCode/exampleCode002 - Copy.λ (7795, 2021-01-21)
data/wikibinator/exampleCode/exampleCode002.λ (1820, 2021-01-21)
data/wikibinator/exampleCode/exampleCode003 - Copy.λ (1820, 2021-01-21)
data/wikibinator/exampleCode/exampleCode003.λ (1820, 2021-01-21)
data/wikibinator/exampleCode/exampleCode004.λ (1820, 2021-01-21)
debugstepinator_old/ (0, 2021-01-21)
debugstepinator_old/Color.java (7810, 2021-01-21)
debugstepinator_old/DebugstepinatorGraphUI.java (607, 2021-01-21)
debugstepinator_old/Node.java (4792, 2021-01-21)
fixingselfreference/ (0, 2021-01-21)
fixingselfreference/Selfref.java (2721, 2021-01-21)
immutable/ (0, 2021-01-21)
immutable/util/ (0, 2021-01-21)
... ...

# wikibinator Newer version at https://github.com/benrayfield/wikibinator104/ (in progress) A decentralized wiki style interactive math book (for ages 0 to expert, which TODO will appear like cartoony art with drag and drop or hardcore number crunching tools that hook into cloud computing tools etc depending on the user's skill), based on a combinator (that is both a universal lambda function and a pattern calculus function of 6 parameters which has vararg lambdas) in which it is extremely easier to say true things than to say false things, based on a logic similar to godel-number where one must commit to statements about lambda called on lambda returns lambda before one can verify which lambdas they are, and in theory scaleable enough for graphics, musical instruments, GPU number crunching, etc, but lets start simple, so everyone can understand and fit the pieces of the puzzle together. Will be built on this layer: https://github.com/benrayfield/axiomforest [[[[[[ [[[[[[ # axiomforest A kind of number completely defined in this sentence, that an axiomforest is an immutable 4-way forest with 2 axiomforest childs and 2 bits which mean Unknown, Yes, No, or Bull, and Bull means simultaneous Yes and No which happens when ORing axiomforests together, and Bull is an error needing forking, and the creation of new axiomforests happens by any chosen function of 2 axiomforests to 1 axiomforest which is a way to change statements from unknown to yes or no but if bull happens anywhere then whatever caused it you need to back out and dont use any set of statements being yes or no which can possibly lead to bull again as converging gradually toward higher consistency. Its for number crunching, experimenting with various kinds of godel-numbering and pattern calculus functions and universal lambda functions (combinators) such as occamsfuncer, wikibinator, iota, unlambda, andOr urbit, and for AIs and neuralnets and neural-turing-machine-like experiments, and virtual worlds computed on GPUs with trillions of threads and exabits stored and flowing data across the internet at gaming-low-lag all as one big sparse bloom-filter where unknown is 00, yes is 10, no is 01, and bull is 11, in each binary forest node, and if you want to say just 1 binary forest node is yes or no then you use unknown (00) in all nodes below it (theres an optimization for it, caching a few extra bits in node ids derived from below) and this node is yes (10) or no (01) which are the 4 TruthValues. Scaleable. Gaming-low-lag. Immutable. Merkle. Near-godel-quality-self-reference. Number. u is the leaf aka thue universal function. (u u) is 0. (u 0) is 1. (u anything_except_0_or_1) is a namespace, such as (u "wikibinator102" ...params...) is where statements about the wikibinator version 1.02 universal function might go, each such statement being unknown, yes, no, or bull, where "wikibinator102" is a complete binary tree (cbt) of 0 and 1 such as (((10)(11))((00)(10))) is the byte 10110010, and from that we can make utf8/unicode text, but only of powOf2 size bitstrings, and view that as the last 1 is just past the end of the bitstring, so 1000000... pads until next powOf2, to define any bitstring. It will support an unlimited number of different kinds of ids, generated by universal functions, or multiple id types at once. For example, you might use the first 30 bytes of sha3_256 of 3 axiomforests, and have 1 byte for its TruthValue, 6 bits for certain caches from below (allYes allUnknown allUnknownBelow allObserve anyBull isLeaf myYesPartOfTruthValue myNoPartOfTruthValue) and have 8 bits for being all 0 if its not a complete binary tree of bits and 254 possible values of its height for bitstrings of sizes 2^0 bits to 2^253 bits (sparse) and if its the byte 255 it means it is still a bitstring but its height doesnt fit in a byte. The third child would be a cache of this same binary forest shape but with all nodes as TruthValue.unknown, which is the normed form of a binary forest shape and can be used to find contradictions or just generally align them. So it would be those 2 bytes then the last 30 bytes of sha3_256 of those 3 axiomforests (the first 2 are childs and the third is a cache of the normed form). You would send 128 bytes at a time, to mean here's the id of an axiomforest and here are its 2 childs and its normed form, or the third is all 0s if its already the normed form of itself, and an id256 can have up to 128 bits of literal data (a complete binary tree of 128 bits) so you can generate the ids of its left and right childs all the way down to leaf without storing them, such as you might store a complex number of 2 float64s in an id256 or 4 float32s or a string of 15 utf8 bytes. Even though an id can only hold 128 bits and with its 2 childs and normed form is 128 bytes to store 16 bytes, the binary storage efficiency will be over 99% since any bitstring tree-hashes to a specific id, given a specific idMaker (which is any halted lambda (which is an axiomforest) that returns a bitstring when its param is an axiomforest [that wraps the actual param axiomforest to make it useable by a halted lambda], and those kind of details vary by namespace. Anyone can read and write anything, but we onky share immutable merkle forest nodes that tend to OR into eachother as long as we expect that wont later lead to any TruthValue.bull. Inside (u "wikibinator102") will be an infinite number of possible halted lambdas, which are themself as the call pairs, like you can see with the L and R and IsLeaf opcodes in https://github.com/benrayfield/wikibinator/ or similar in https://github.com/benrayfield/occamsfuncer or in urbit etc. Any of those, and any system at all could in theory be translated into sparse bloom filter form, but each node can only be written once, as yes or no, except that it can be written an infinite number of times as long as they all write the same value of yes or all no and any of them can write unknown since that doesnt change yes or change no or change bull. Anything thats not halted must be some other data structure (see debugStepInto and debugStepOver both in wikibinator (todo) and occamsfuncer (OcfnUtil.java has that working, using 2 callquads together, one as a state of the stack and one as a cache of func called on param gives return value which the stack state is looking for what happens when call that func on that param), within the binary forest than its literal call pairs, since all axiomforests are halted, and all work comes in bigO(1) constant size pieces that you might put in a java.util.function.BinaryOperator or in a javascript or python function of 2 objects to 1 object. Its not specific to any of these languages. Its just a bloom filter with 2 bits at each possible binary forest node and a merkle forest for each possible state of a node and possible states of all nodes reachable downward through L and R child pointers down to leaf, each with a specific TruthValue (unknown, yes, no, bull). (u "mutuallyAssuredDestruction" 0 x y z) -> z is No, or if its 1 instead of 0 as that param then it proves z is Yes (you can prove both, just do both of those separately, therefore proving z is Bull, which expands exponentially as mutuallyAssuredDestruction can use z to prove anything else is Bull, and so on, until the whole p2p network is bull and to avoid that happening people and computers will become very motivated to have exactly 0 bull in the network or to converge quickly to it before the mutuallyAssuredDestruction spreads, or if they dont like this axiom which might be viewed as too fast and too extreme then it can also be proven to be No and therefore unuseable), if x and y are the same forest shape and 1 of x and y is Yes and the other is No aka Bull, which is correct logic since thats a proof that Yes equals No, and using Yes equals No you can prove absolutely anything, which is what the "mutuallyAssuredDestruction" namespace is for, proving everything that its asked to prove using a proof that yes equals no. ]]]]]] ]]]]]] https://github.com/benrayfield/wikibinator/blob/main/wikibinatorV0/datastructsBeforeCompileThemAllToAxiomforest/nodes/InfiniteSetContains.java ``` /** This can be used to ask a turing-complete question of "find a param of a certain function which when that function is called on it the call halts". For example, if you just want to call x on y using this, then the function would call x on y then compare its param (using derived equals function) to what that returns (if it ever returns), which an optimization could be designed for to understand that you are just asking the question "what does (x y) return?", but in a unified way that might be more optimized, that all questions to the system would be of the form: find an InfiniteSetContains where InfiniteSetContains.infiniteSet()==theGivenFunc, like the "occamsfuncer nondet solve" function.

f contains p if (f p) halts, therefore Rfpd implies an InfiniteSetContains. f contains p. All such infinite sets (that can be represented in this system) have finite kolmogorovComplexity. An infinite set can contain itself or not. There are no paradoxes, such as it is not possible in this system to ask https://en.wikipedia.org/wiki/Russell%27s_paradox cuz it is "word salad". Not every sequence of words means something.

TODO??? if this were to have 2 possible return values, T and F (which theres an axiomforest form of T and F and a wikibinator form of T and F at a higher level, which are different things), instead of just halts or not (aka halts on T or halts on F or [does not halt or halts on something other than those]), then this could be viewed as the set of all possible hash functions of 1 bit each (allowing unknown if it doesnt return T or F on a given possible param) such as the 237th bit of sha3_256 of a certain merkle forest node (with some pre and post processing) etc, then various functions could name eachother by their T or F (if they return at all on eachother) so every tiny part of every possible hash algorithm could hash every tiny part of eachother, the same way as you could ask for a solution to any (finite kolmogorovComplexity) puzzle. The T vs F could be viewed as the param is certainly in the set, or certainly not in the set, vs if its not been observed to return yet (or will never halt) then its unknown if is in the set or not. */ public class InfiniteSetContains extends AbstractNode{ "TODO T F kind vs simplerDoesItHaltOrNot kind" public InfiniteSetContains(HaltedLambda infiniteSet, Node memberOfSet){ super(infiniteSet, memberOfSet); } public HaltedLambda infiniteSet(){ return (HaltedLambda)get(0); } public Node memberOfSet(){ return get(1); } public Node step(){ return this; } } /** a claim that a certain Callquad (a nonhalted lambda call) will not halt. You may Believe.java this or claim it without a Believe (as you may claim anything with or without a Believe, but if you claim it and a Rfpd is found where it does halt, then (TODO create a MultiReturnDetector for nonhalting vs halting on a specific value, or should Rfpd be able to represent nonhalting such as using (S I I (S I I)) which is a callquad as the normed form all nonhalters?). TODO add an axiom that (S I I (S I I)) WontHalt, and an axiom that anything which has a nonhalting child callquad is itself nonhalting (even if it ignores that callquad such as (T x anythingThatHalts)->x but (T x anyNonhalter) does not halt.

There are a few general categories of halting vs nonhalting...

-- halter (a kind of infiniteLoop of length 1 since x.step->x).

-- infiniteLoop (length > 1) which are anything where x.step.step.step... leads back to x.

-- leadsToInfiniteLoop which is anything which does not come back to itself but leads to an infiniteLoop.

-- foreverExpander which is any nonhalter that is not a infiniteLoop or leadsToInfiniteLoop.

If x is a halter or infiniteLoop or leadsToInfiniteLoop, that can be proven in finite time and memory (though may be so large a "finite" number that we would never figure that out).

The last 3 of those 4 things WontHalt. TODO be more specific about it? */ public class WontHalt extends AbstractNode{ public WontHalt(Callquad call){ super(call); } public Callquad call(){ return (Callquad)get(0); } } /** This can be used in parallel such as (S x y z) evals to ((x z)(y z)) aka (x z (y z)). Each of (x z) and (y z) may be an S call, which is very common, so could continue becoming more parallel, or do it sequentially. Each such call can be precomputed such as by lwjgl opencl GPU optimization, to create a Rfpd for (x z) and a Rfpd for (y z) so if both of those already exist then they can be used with 2 DebugStepOver (created by 2 GetRfpdfromCallquadIf, from the callquads it was computed in), so it is still 2 sequential steps of CallQuad -> DebugStepOver -> CallQuad -> DebugStepOver -> CallQuad, but thats bigO(1) and those DebugStepOver can each be any huge amount of work done in parallel, and together they generate a Rfpd of the whole (S x y z) call which can be used the same way anywhere someone wants to know what happens when you call (S x y) on z, what does that return, the Rfpd tells the returnValue for that (func param), and if someone makes up a fake return value, then those 2 Rfpds can go in a MultiReturnDetector which will check (in STEP from it) if they both have the same func and param but different returns, and if they do then it proves that the axiom TruthValue of No is Truthvalue.yes (and its also Truthvalue.no), and many MutuallyAssuredDestructionIf already each have 2 childs: No and anyRandomlyChosenNode, and No (if its yes) implies anyRandomlyChosenNode is the NOT of its current TruthValue (or implies its both separately, todo choose a design, should it have to know a current yes or no to choose the opposite or just do both in 2 separate STEPs), so thats what protects the system from people andOr computers making up, or just accidentally computing it wrong, the wrong returnValue for a (func param) lambda call, which is most likely to happen or be used by DebugStepOver and Rfpd.

datastructThatSomehowDoesDebugstepoverUsingSomethingLike2CallquadsButTodoWhich2SpecificDatastructs. */ public class DebugStepOver extends AbstractNode{ /** If cacheKey's func and param matches the func and param the call wants to know returnVal for, then this IMPLIES far ahead in the calculation aka debugStepOver it instead of debugStepInto, but if its not a match then this IMPLIES (todo choose a design, either debugStepInto or implies some constant thats always true). */ public DebugStepOver(Callquad call, Rfpd cacheKey){ super(call, cacheKey); } public Callquad call(){ return (Callquad)get(0); } public Rfpd cacheKey(){ return (Rfpd)get(1); } public Node step(){ //new GetRfpdFromCallquadIf(call()).step() if( call().func().equals(cacheKey().func() && call().param().equals(cacheKey().param() && (HaltedLambda) .. (call.func call.param).isHalted ){ //do debugStepOver, returning a HaltedLambda "then return that (HaltedLambda) .. (call.func call.param).isHalted" }else{ //is not the cacheKey needed or was not ready to debugStepOver throw new RuntimeException("TODO return this? or do a debugStepInto? Or return Yes (no-op)?"); } } } /** This system cant prove its own correctness, but if an axiom generates an axiom that generates an axiom that generates an axiom ... many levels deep, it is still possible to trace it back to the set of axiomforest nodes which led to this node, the same as if they were not generated axioms but just data generated by a single axiom, since code is data, and if no MutuallyAssuredDestruction (blockchain-fork or bits of logic forking in 1 computer) happens while being extremely redundantly cross-referenced by turing-complete-challenge-response, then we can gain confidence over time that some set of axioms (that generate axioms that generate axioms) never generate anything that contradicts anything else (TruthValue.bull).

This system does not provide a way to generate the first GeneratedAxioms but does provide a way for various people andOr computers to experiment with combos of them and see if contradictions are found, and choose to continue that in various combos. The way you do that is add an axiom where Yes implies a specific GeneratedAxiom, which might (TODO choose a design) fit in a Rfpd or something similar to a Rfpd which is the same way Rfpds in the wiki are added since wiki (1 of the wikibinator opcodes) is the only nondeterminism in the system (except maybe statements in the axiomforest that cant be proven or disproven?). I'll create a Node type for that right now, which is called Believe.

datastructWrappingAHaltedLambdaInThe(Axiomnode.v)Child)ThatsClaimedToBeAValidAxiomBased OnTheVShapeAndStepFuncCreatesWhateverItSaysToWithoutVerifyingIt */ public class GeneratedAxiom extends AbstractNode{ public GeneratedAxiom(HaltedLambda callThisOnA_ViewNodeAsHaltedLambda){ super(callThisOnA_ViewNodeAsHaltedLambda); } public HaltedLambda callThisOnA_ViewNodeAsHaltedLambda(){ return (HaltedLambda)get(0); } } /** In some cases (depending what is halted), (callquad.cacheKey.func callquad.cacheKey.param)->(callquad.func callquad.param). (callquad.func callquad.param) is a HaltedLambda. (callquad.cacheKey.func callquad.cacheKey.param) is normally a HaltedLambda but technically might be nonhalted aka a callquad with no stack (is it null or leaf or what constant?) and no cacheKey.

TODO should callquad be used directly as Rfpd instead of this class? */ public class GetRfpdFromCallquadIf extends AbstractNode{ public GetRfpdFromCallquadIf(Callquad call){ super(call); } public Callquad call(){ return (Callquad)get(0); } public Rfpd impliesRfpd(){ throw new RuntimeException("TODO read comment of this class, and return null if it doest imply that, else generate the Rfpd it implies"); } } public class HaltedLambda extends AbstractNode{ public HaltedLambda(Node func, Node param){ super(func,param); } public Node func(){ return get(0); } public Node param(){ return get(1); } } /** No, Yes, T, and F, are 4 different things. Yes, T, and F are axiom value TruthValue.yes. No is axiom value TruthValue.no, or is TruthValue.bull when used as a peaceful-just-forking mutuallyAssuredDestructionTrigger.

You should have these MutuallyAssuredDestructionIf nodes pointing from No to every other Node (at least in abstract math) or randomly selected nodes, which force blockchain-fork or logic-in-1-computer-fork if any BULL is proven, to fork to a possible state of the system which is less likely to have any BULL, and many possible states (merkle forest nodes) explored in many combos at once, so mutually assured destruction is about a "multiverse branch" and you probably wont even notice it cuz theres so many of them happening at once, like "error correcting codes" except in a more extreme way to motivate convergence toward 0 errors in the p2p network. Errors slow things down and break compatibility and the whole system would destroy itself if it wasnt instantly ready to back out of any even slightly wrong calculation in many combos. This is like the "control rod" of the wikibinator system and it operates at a precision between .01 seconds and .00001 seconds, closer to .00001 except when OS gives another thread control for a short time or during lwjgl opencl gpu optimizations that do a block of calculations such as in .005 seconds. The worst that will happen ... ...

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：