We're still under construction!
And you just found out where. We're still working on this page. How did you get in here, anyway?
λ-chain
Naturally distributed computing.
Welcome to the Lambdachain!
Lambdachain takes the statement a well-typed program always halts and extends that type-safety to that of origin-safety, in order to enable security and privacy in naturally distributed computing.
With this, we are building a compiler thas allows for efficient logarithmic scaling of distributed networks without requiring specialized 'smart contract' programming of storage, networking, and APIs. It does this using proofs that reduce down to a single value as small as a single key hash or equation. This allow for the state of complex objects to be maintained via key small enough to embed in cheap hardware like smart cards or Yubikey, no matter how large the system.
A Turing-complete model of distributed computation.
Lambdachain is a naturally distributed model of lambda calculus (a turing-complete method of computation) that extends the concept of a type-system into that of an origin system in order to generalize algebraic variable substitution over the concepts of CPU registers, RAM pointers, FILE paths, URL addresses, and blockchain hashes, using a proof that they are interchangeable. It is a true generalization in which we are free to substitute any homomorphic naming schema, including equality, isomorphism, adjunction, and cryptographic hashing.
Work with strongly-originated and strongly-typed facts, not anonymous binary files.
Untyped binary data is by now obviously insufficient for today's computing needs. Lambdachain is based on higher-order laws that apply to all data and computation, enabling security and provability in ways that we can not with the standard approach of untyped binary.
Persist any computation to the distributed lambdachain.
Don't write APIs and network code. Let the compiler do that work for you. Because of its basis in higher-order theory, lambdachain works for all well-defined types of data, and can automatically derive programming interfaces using minimal type annotations and free theorems.
The future of computation
Lambdachain is naturally distributed in the sense of both natural numbers, but also in a sense that it is the ultimate reduction of distributed computation.
The future will have to contend with computation in many forms - analog, digital, statistical, quantum, machine learning. These are all computation, and should integrate smoothly with each other as equations do - we will never achieve things like superscaling and mind uploading unless we unify them all, and it is painfully obvious that our current computer architecture is not up to task.
It is our hope that lambdachain enables the better scaling of distributed computation on silicon, but also furthers the science of information theory, machine learning, and neuro-cognitive sciences in general, as a means of exploring questions such as 'how do systems as large as the brain naturally perform distributed computation over trillions of cells', or 'where is the knowledge / data in Searle's room'.
Lambdachain: In depth
What is lambdachain?
Lambdachain is the naturally distributed (as in distributed network) extension of lambda calculus generalized over a few characteristics.
- 1) We then subdivide the dimensions the concept of a `type` system into an `origin` system, where statements are aware of not just `what` they are, but also `who` stated them, and more. This allows for the creation of statements that are `strongly-originated`.
- 2) We use homomorphic naming of variables / expressions that are `strongly originated`. That is, statements in which `who` said it is embedded into the very `what` that was said.
- 3) We model computation as occuring over statements of `sets of strongly-originated facts`, rather than statements of states of objects / machines.
- 4) We allow that `strongly-originated facts` may be pruned when they are provably irrelevant, allowing for distributed systems without requiring that they be append-only.
This enables a `set of originated facts` model of data computation which may be information-theoretically maximally efficiently stored, transfered, and proven over any distributed network, maintaining validity of the data without requiring foreknowledge of the structure or trustworthiness of the network (while still being able to compile for speed when necessary).
This generalizes over category of every known computional class, and relies on the deeper fundamentals of what computation really means in order to achieve that. Lambdachain is more than just `type-safe`, it is `origin-safe`.
Why is lambdachain?
Traditionally, computers are viewed as turing machines, which can lead to requiring large descriptions in order to model computation as objects. This has been the default view for the last century.
Lambdachain is a compact definition of distributed computing, requiring very little to implement while remaining capable of being compiled to high-speed, machine-specific assembly. It allows for ultimate code reusability, in a perfectly reproducible environment. This is in contrast to more machine-perspective implementations, which are by definition larger and harder to prove but yield no additional power, while remaining difficult or effectively impossible to prove anything about its behavior.
How is this useful? An increasingly pertinent example is quantum supremacy. Quantum supremacy will break some algorithms, and they will need to be proven for other algorithms. Lambdachain allows for the algorithm to be part of the type system, and thus can reuse its algorithms by simply using homomorphic hashing and computation, which is quantum-resistant.
How do we lambdachain?
Lambdachain is not yet available - we're still working on a singular compiler implementation after spending years proving all of the individual pieces necessary to construct it. Building it is hard - if it were easy, somebody else would have done it by now.
We're targeting implementations in Haskell, Javascript, and C, and this is going to take some time. We're expecting to have a proper demonstration of at least one implementation available by late 2022, or early 2023. Come back before then, though - we'll get something for you to try out sooner rather than later.
Where can we learn more?
A deeper understanding of the lambdachain requires advanced knowledge of functional programming, lambda calculus, type theory, category theory, and a firm grasp on concepts of the relationship between turing completeness and recursion. We'll do our best to provide these prerequisites in coming future articles.