-The blockchain is a novel approach to support distributed systems enabling a common, consistent view of a shared state among distributed nodes. There, smart contracts are computer programs that allow users to deploy arbitrary computations, in charge of automatically regulate state transitions and enforce properties. In this paper we speculate on how the blockchain and smart contracts could take advantage of a logic programming approach, and, complementarily, on how logic programming can benefit from the blockchain infrastructure. Accordingly, we discuss some possible research directions and open questions for future research. Index Terms-blockchain, logic programming, smart contracts.
The blockchain technology (BCT henceforth) gained
attention as the backbone of cryptocurrencies such as Bitcoin [
A popular categorisation of blockchain models orders them
in three generations [
The implementation of smart contracts offered by nowadays
BCT constrains users to express their business logic by means
of object-oriented programming (OOP) abstractions and an
imperative programming style—both strictly bound to the
underlying BCT. In the following we take Ethereum2 as
our reference as the most well-known framework for smart
contracts currently available [
We suggest that the choice of OOP may have hindered the
full realisation of the expectations related to third generation
BCTs. In fact, smart contracts were originally conceived as
a means to automatically enforce the conditions defined in a
contract, and to guarantee invariants and properties despite
the ever-changing state of the blockchain [
So, there seems to be a mismatch between the computational model chosen for Ethereum’s smart contracts and the one actually fitting their original requirements and intended purpose. Among the many programming languages and computational models available – as Solidity4 for Ethereum, Go for the Hyperledger Fabric5, or Java for Corda6 – a declarative language backed by a logic programming computational model could be best suited for both (i) expressing high level policies in an unambiguous and human-readable way, and (ii) supporting inference and sound demonstration of properties of interest. In turn, as a distributed ledger technology, the blockchain could bring to distributed logic programming more than a few desirable features, such as consistency, accountability, and fault tolerance.
Accordingly, in this paper we identify the research opportunities arising from re-interpreting the blockchain from a logicbased perspective: on the one hand, how logic programming can improve the capabilities of the blockchain and, especially, of smart contracts; on the other hand, how logic programming may benefit from the blockchain, either as a distributed computing model or as an infrastructure.
The reminder of the paper is therefore organised as follows: Section II provides an overview about the main elements of BCTs and the smart contract abstraction, Section III introduces our vision of logic-based smart contracts, describing how logic programming would provide some useful properties, in Section IV we discuss how the BCT introduces novel ways to face well-known issues of the distributed logic programming research area, and, finally, Section V concludes the paper.
3As detailed in the next section despite the similar name, our notion of
logic-based smart contracts differs from the one proposed in [
The key point is that the blockchain endows applications with highly desirable properties such as immutability and untamperability of the past, consistency among nodes of the system state, fault tolerance of both data and computations. In the following, we describe the elements actually enabling these features, which are: the system (or world) state the transactions describing state transitions the blocks forming an ordered ledger containing all the events that occurred within the system the consensus mechanism (or protocol) smart contracts (3rd generation blockchain only)
States represent what is true for the system at a given instant in time. All nodes composing the system must eventually perceive the same system state. Generally speaking, it is a mapping between the entities’ identifiers – i.e. users – and some arbitrary data associated to and controlled by that entity, there including smart contracts data and code, or user balances.
Transactions encode the state variations yet to be performed. A transaction can apply to a state producing a new state. Nodes may issue (publish) transactions in order to produce an effect on the system state. Transactions may represent money transfer from an entity to another, the deployment of a smart contract, or the invocation of an already-deployed smart contract.
When a transaction is published, it is replicated over the whole system, thus making every node aware of it. However, a transaction can be applied only if it is valid, that is, well formed and correctly signed by the issuer. Otherwise, it is simply dropped, thus preventing unauthorised actions to carry on. Furthermore, to produce an effect on the system state, transactions must be executed without errors, otherwise their modifications to the system are simply reverted. As an example, suppose an entity is trying to transfer more money than it currently owns, by means of a transaction. Such a transaction would eventually throw an error provoking the money transfer and any other side effect to be reverted.
Blocks are timestamped lists of transactions. As such, they
certify (i) the ordering of edits applied to the system state, and
(ii) that each transaction occurred at a specific instant in time,
and therefore the resulting state is valid from that moment on.
Blocks implement the timestamping schema described in [
In fact, locks are replicated on all the nodes thanks to the blockchain protocol, which is in charge of ensuring that the last block – containing the most recent transactions – is the same for each node.
The distributed consensus protocol makes sure that the
distributed nodes – the miners – achieve a common view of
the sequence of blocks, and, consequently, of the ordering
of transactions: in short, its task is to guarantee consistency
in spite of system state replication. While several consensus
mechanisms exist, their detail is outside the scope of this
paper: we forward the interested reader to [
For what concerns the following discussion it is sufficient to understand that BCTs supporting cryptocurrencies (such as Ethereum) usually employ the Proof-of-Work consensus approach, which (i) endows the cryptocurrency with its economical value, (ii) provides probabilistic and eventual consistency of the system state, and (iii) makes the blockchain resistant against Byzantine nodes and Sybil attacks.
Smart contracts consist of stateful processes that can react to the publication of a particular kind of transaction: invocation transactions. For an invocation transaction to be valid, the triggered computation must terminate without errors: otherwise, its effects are reverted, leaving the system state unaltered.
Smart contracts can be conceived (and usually are) as objects in the OOP sense, thus their invocations as method calls. Nevertheless, deployment is quite peculiar: their programs are written and published by end users by means of deployment transactions, publishing the compiled source code (or, bytecode) of a smart contract. In Ethereum, smart contracts are usually programmed with Solidity, which is indeed an object-oriented language. The Solidity code is compiled into the Ethereum Virtual Machine (EVM) bytecode before deployment and the latter is deployed on the blockchain network. Thanks to transaction signatures and blocks hash links, the code of smart contracts is immutable after publication. This is what makes them amenable of trust in, e.g., handling financial transactions: indeed, since the source code is publicly inspectable and immutable, anyone can check the bytecode obtained (i.e. via a disassembler).
Miners are the peer nodes composing the backbone of the blockchain network by participating into the consensus mechanism. They locally store a copy of the whole blockchain – there included a copy of each smart contract – and execute all transactions. Since the system state must be kept consistent among all the miners, each of them locally executes smart contracts upon reception of invocation transactions. Therefore, the execution of non-terminating computations must be prevented, since it would imply a deadlock of the whole blockchain network. The most notable solution is the one introduced by the Ethereum platform, where each computational step is paid by the initiator of the transaction in terms of gas— converted from the initiator balance. Executions running out of gas invalidate their invoking transactions but still consume the initiator’s money.
These money can be redeemed by the first miner producing
the next block of the blockchain, as a compensation for the
computational effort. So, long/infinite computations become
economically unsustainable. This mechanism highlights the
aspect of the economical cost model of computations, which
is currently instruction-based [
III. LOGIC PROGRAMMING FOR SMART CONTRACTS We now introduce the idea of logic-based smart contracts as an intriguing research perspective, highlighting its challenges and possible benefits. It is worth remarking that we do not mean to produce “yet another compiler” for a logic language to EVM, but to replace the EVM itself with a logic engine and related computational model, so that smart contracts can be expressed in a logic language—e.g., Prolog.
We see three major motivations for doing so: (i) the declarative nature of the source code, (ii) observability of the business logic, and (iii) controlled mutability of behaviour.
Adoption of a declarative language with a goal-oriented semantics could ease both developers’ work and readers’ understanding in general: the former would be able to explicitly state the business goals the smart contracts should pursue – which could in turn be able to share them or reason about how to reach them –, while for the latter would be easier to understand the functioning of already-deployed smart contracts. Furthermore, since Prolog is an interpreted language, it could also help strengthening trust via improved inspectability: in fact the source code may be deployed with no need of compilation, and it would not require any disassembler for being inspected later on.
By endowing logic-based smart contracts with a static
knowledge base (KB) containing immutable rules and terms,
alongside a dynamic KB containing the mutable ones, smart
contracts could be structured in such a way to partially modify
their behaviour in a controllable way. A practical example
of such an interesting feature is extensively described in
Subsection III-C. This helps mitigating the problems caused by
buggy smart contracts that are deployed and, being immutable,
cannot be fixed—anyway, a practice considered harmful [
As a first step towards our vision we need to re-interpret the blockchain elements summarised in Section II according to a logic-based perspective. To this end, let us suppose that the system state maps smart contract identifiers into some data structure, including at least a balance to enable smart contracts to handle money, a static KB made of an immutable list of logic facts and rules, to be set upon deployment, and an initially empty dynamic KB which may be modified via assert/1 and retract/1 money transfer transactions retain their semantics, whereas smart contract invocations become goal-oriented computations as described in the following blocks and consensus retain their semantics As a second step, we need to define the behaviour of logic based smart contracts, that is, how they react to transactions. While money transfer transactions retain their semantics, invocation transactions can be supposed to specify a logic term, say Message, that triggers a goal-oriented computation Goal if the KB of the invoked smart contract contains a rule such as receive(+Message, +Guard):- Goal. provided that Guard is true. If no such a rule is found, the transaction is considered invalid and it produces no effect.
The computation (Goal) is performed according to the
usual SLD resolution process [
The third step should focus on inter-smart contract
interaction. As the reader may expect, a send(+Recipient,
?Message, ?Money) primitive has been conceived too,
which can be used by a smart contract to send a Message to
another one (namely Recipient), possibly including some
Money, therefore triggering one of its receive(Message,
Guard) entry points. An interesting aspect which may be
worth of further investigation is whether the send/2 primitive
should have a synchronous or an asynchronous communication
semantics. In the first case, the inter-smart contracts interaction
semantics would redeem their OOP-like nature, along with its
well known re-entrancy issues [
The semantics of blocks and of the consensus algorithm remain unchanged: this implies no interference while a resolution process is being executed, since transactions are totally ordered and sequentially executed. The miners’ role, too, remains unchanged: simply, in this vision they are in charge of the SLD resolution process. However, removing the EVM bytecode from the picture opens up the possibility of defining a more coarse-grained computation cost model, taking into account the specific features of the logic-based computational model—with the usual aim of discouraging long computations. For instance, should users pay for the proofs to their queries? Should they pay for unification of clauses and facts? What about paying for backtracking? These questions have no trivial answer at the moment, thus deserve further research.
As an illustrative example, consider a scenario where the flight company ACME Inc. exploits smart contracts for regulating costumer management. The company handles purchase of tickets through its ACMEPortal smart contract, which provides a number of functionalities, among which: 1) looking up for flights towards a given destination (To) within a given timespan (Day): receive(look_up(Day, From, To), (now(Now), after(Day,
Now))) :setof( flight(Id, Time, Duration, From, To, Price), (flight(Id, Time, Duration, From, To, Price), within(Time, Day)),
Flights ), sender(Customer), send(Customer, Flights, _). where within(+TimeSpan, ?Instant) simply checks whether Instant is within TimeSpan. 2) reserving a seat paying the corresponding Price: receive(reserve(Id), (flight(Id, Time, Dur, From, To,
Price), value(X), X >= Price)) :sender(Customer), assert(reservation(Customer, flight(Id, Time, Dur,
From, To, Price))). 7http://solidity.readthedocs.io/en/latest/units-and-global-variables.html 3) cancelling a reservation while getting a refund, possibly with a fee if cancellation occurs later than 3 days before expected departure: receive(cancel(Id), (sender(Customer), reservation( Customer, flight(Id, ExpDeparture, _, _, Price))) ) :now(CurrentTime), retract(reservation(Customer, flight(Id, _, _, _, _) )), compute_refund(CurrentTime, ExpDeparture, Price,
Money), send(Customer, _, Money). where computation of the amount to refund is encapsulated by the compute_refund/4 predicate, assumed to be in the dynamic KB of the smart contract: compute_refund(CancellationTime, DepartureTime, Price,
Price) :
DepartureTime - CancellationTime > days(3). compute_refund(CancellationTime, DepartureTime, Price,
ToBeRefunded) :DepartureTime - CancellationTime =< days(3),
ToBeRefunded is Price / 2. 4) automatically getting a refund in case of delays longer than some given amount of time: receive(landing(flight(Id, ExpDeparture, Dur, _),
ActualTime), true) :setof( refund(Customer, Price), (reservation(Customer, flight(Id, ExpDeparture, Dur, _, _, Price)), too_late(ExpDeparture, Dur, ActualTime)),
CustomersToBeRefunded ), refund_all(CustomersToBeRefunded). where refund_all/1 is a simple broadcast: refund_all([]). refund_all([refund(Customer, Price) | Rs]) :send(Customer, _, Price), refund_all(Rs).
To support functionality x4, airports are assumed to deploy a AirportNotification contract in charge of notifying ACMEPortal about the actual departure and landing times, by sending messages in the form: departure(flight(Id, ExpDeparture, Duration, FromAirport),
ActualDepatureTime) landing(flight(Id, ExpDeparture, Duration, ToAirport),
ActualLandingTime)
Functionality x1 collects all flights information matching a custom filter. For instance, users may ask for all the flights departing from a given place on a given day by providing an unbounded To variable as input. The operation also shows how contextual predicates may be useful to implement userand time-aware operations.
Functionality x2 shows how to add new data to the dynamic KB of the smart contract. Notice that, since functionailities are wrapped within the receive/2 primitive, no entity except the smart contract itself can add (or remove) information to its KB. This is how encapsulation of smart contracts KBs, i.e., their states, can be achieved.
Functionality x3 shows the dual operation, namely, how to remove data, while illustrating what we mean by controlled mutability. Suppose ACME Inc. wants to adopt a different policy for cancellations. Assuming the smart contracts exposes one more functionality: receive(compute_refund(C, D, P, T) :- NewPolicy), (sender(S ), authorised(S))) :retract_all(compute_refund(_, _, _, _) :- _), assert(compute_refund(C, D, P, T) :- NewPolicy). then it would be easy for the IT department to dynamically inject the novel policy as a replacement of the previous one. In Ethereum, for instance, such a flexibility is not possible without carefully engineering some cumber-stone interaction pattern between two or more smart contracts.
Finally, functionality x4 illustrates how to compose smart contracts declaratively to give a refund to customers in case of delayed flights, automatically. This is an example of intersmart contracts interaction through the send and receive primitives involving more than two smart contracts.
IV. THE BLOCKCHAIN FOR LOGIC PROGRAMMING We now switch perspective w.r.t. previous section, that is, we explore the idea of exploiting the blockchain technology to face some well-known issues of logic programming in distributed systems—namely, consistency of a distributed, possibly dynamic logic theory which evolves over time, and concurrent reasoning. The blockchain may support for instance cooperative exploration of the proof tree for a given goal, while smart contracts may be the key for letting different, para-consistent theories coexist within the same system. As a first intuition, the blockchain can act as the mediator giving distributed access to the logical theory representing the knowledge to share.
In the following we discuss two distinct scenarios: in the first, the ledger is re-interpreted as a single distributed logic theory where nodes may participate to the resolution process, while in the second, smart contracts are conceived as containers of immutable logic theories.
Several approaches for distributing logic programming have
been historically explored, in particular towards implicit
parallel evaluation, leading to explore AND-parallelism and
ORparallelism [
The blockchain model and technology could open up new perspectives in the distribution and parallelisation of the resolution process with respect to a single theory shared between different participants of the distributed system. In this vision, a first intriguing possibility is to distribute the goal to solve over the blockchain: the blockchain system is so re-interpreted as an inference engine coordinating a number of processors – the miners – aimed at (i) handling users’ assert, retract, and solve requests, or (ii) carrying on goal proving processes by concurrently exploring different paths of some goal’s proof tree. We therefore imagine transactions as: information creation/consumption, in the form of logic clauses, to the distributed ledger—e.g., assert(?Clause)/retract(?Clause) inference invocation aimed at triggering a resolution process on a given goal—e.g., solve(?Goal) At the same time, miners are re-interpreted as the entities in charge for repeatedly performing partial explorations of the proof tree or producing solutions for provable sub-goals. By keeping track of already proved (sub-)goals too – on the ledger – miners can avoid wasting their computational resources proving what has been proved by others.
Finally, economical incentives could be designed and tuned to stimulate a particular joint exploration strategy of the proof tree. For instance, the blockchain protocol may initially reward the most miners exploring novel branches of the proof tree or finding solutions for unproven (sub-)goals, but, after that, it may also start encouraging miners to keep exploring the same path of the proof tree, in order to minimise the probability of two ones competing to prove the same (sub-)goal.
Although our vision appears to be feasible in practice,
further research is needed when facing the theoretical foundations
of cooperative reasoning on top of a blockchain. In particular,
the lesson learned from concurrent logic languages such as
Concurrent Prolog [
All the above blockchain benefits in guaranteeing properties
like consistency can be re-thought in a multiple theories
scenario, where consistency is referred to the local situation, for
instance. There, diverse logical theories are scattered around,
representing the local knowledge of each node situated in
space and time [
In this context, each theory would be associated to a group of local agents, and possibly merged with other computations in the system only once the result is computed: there the blockchain technology could help in integrating data, and guaranteeing properties like local consistency.
Indeed, smart contracts could play a key role to
guarantee the consistency (or other relevant properties) of a logic
theory replicated on the subset of network nodes in a “logic
neighbourhood”: in fact, a smart contract running every time a
change to the theory is proposed could help deciding whether
the change should be accepted or not. There, the smart
contract could also manage assert/retract on the knowledge
base, ensuring the (eventual?) consistency of the shared theory.
Other examples of properties that could be enforced by such
a mechanism are invariants and computational properties like
stratification [
On the one hand, the blockchain could benefit from logic programming to obtain system properties like observability, explainability, and evolvability. On the other hand, blockchain and smart contracts look as promising technologies to exploit the full potential of distributed LP. Accordingly, this paper elaborates on how blockchain and smart contracts could mix with logic programming, and foresees a number of lines of future research on the subject.