eyeprolog

Linear logic with resources

Can a rule use each resource exactly once?

Ordinary logic lets a fact be used as often as you like. Linear logic treats facts as resources that are consumed. This example models that inside Prolog: it bakes bread from wheat, yeast and heat, and shows that one coin cannot pay for two purchases.

Run it in the playground · Source

The question

A kitchen holds wheat, yeast and heat. Can a three-step plan turn them into exactly one loaf of bread? And can a wallet with one coin buy both flour and yeast?

In classical logic the coin could be “used” twice. Linear logic forbids it, and so must the model.

Resources and rules

initial(kitchen, [wheat, yeast, heat]).
initial(wallet, [coin]).

linear_rule(mill, [wheat], [flour]).
linear_rule(mix, [flour, yeast], [dough]).
linear_rule(bake, [dough, heat], [bread]).
linear_rule(buy_flour, [coin], [flour]).
linear_rule(buy_yeast, [coin], [yeast]).

A state is a list of resources. Each linear_rule/3 is an encoded linear implication: its inputs are used up and its outputs appear.

Consuming resources

consume_all([], State, State).
consume_all([Need | Needs], State0, State2) :-
  select(Need, State0, State1),
  consume_all(Needs, State1, State2).

linear_step(State0, Rule, State2) :-
  linear_rule(Rule, Inputs, Outputs),
  consume_all(Inputs, State0, Rest),
  append(Outputs, Rest, State2).

select/3 removes one occurrence of a resource. If the resource is not there, the step fails. That is the whole “use exactly once” discipline.

The answer

eyeprolog examples/linear-logic-resources.pl

linear_result(kitchen, [mill, mix, bake], [bread]).
linear_check(double_spend_rejected, yes).

Milling, mixing and baking leave exactly [bread]. And no two-step plan can buy both flour and yeast with one coin.

The reason

eyeprolog --proof examples/linear-logic-resources.pl

step(linear_check(double_spend_rejected, yes),
     rule(14),
     ['State' = [coin]],
     [initial(wallet, [coin]), \+ run_linear(2, [coin], [buy_flour, buy_yeast], _finalstate)]).

The double-spend check holds because the wallet starts with [coin] and a complete search for the plan [buy_flour, buy_yeast] found no way to run it.

The check

condition('C6', boundary_consistency, ok, 1).
steps(38).
verified(22).
recomputed(15).
trusted(1).
claims(2).
verdict(checked_with_obligations).

The bread plan is fully replayed. The double-spend result rests on one negation, \+ run_linear(2, [coin], ...), reported as an obligation: a proof can show that something was derived, but “no plan exists” is the outcome of a completed search. The checker found no evidence against it.

Try it

Put two coins in the wallet (initial(wallet, [coin, coin])). The double-spend check now gives no answer, because both purchases succeed.
Add a rule linear_rule(sell, [bread], [coin]) and plan from wheat to coin.
How would you represent a resource that may be reused, like an oven, in the same model?

Learn more in The Art of EyeProlog, Chapter 24.

This site is open source. Improve this page.