Hey Christian,
Love this chain of thought! Back before I'd realized as ZmnSCPxj did that
we have a nice general NOT operation for a given point, I had a similar
thought on this thread
https://lists.linuxfoundation.org/pipermail/lightning-dev/2019-October/002213.html
where we eventually figured out that verifiable encryption kind of yields a
nice OR operation (where addition gives a nice AND).
I would like to note a couple of unsolved things/limitations on this front
though. The current NOT operation actually isn't composable meaning If I
have P_1 and P_2 we know how to construct !(P_1 AND P_2) but I don't
believe we know how to do (P_1 AND !P_2). This is because NOT P is
essentially an unconditional payment atomic with a reverse "cancellation"
payment using P as its payment point.
Looking more closely at ZmnSCPxj's proposal for escrow contracts which we
were previously thinking of as (Seller AND (Buyer OR Escrow)) I believe is
actually essentially just a payment to the Seller using the point !(Buyer
AND Escrow) as opposed to some actually compiled version of (Seller AND
(Buyer OR Escrow)).
All of this said, I think it would be super awesome if someone thought of a
way to construct some kind of negation operation which is composable in the
sense that we can do (A AND NOT B) and/or (A OR NOT B) or the like!
Best,
Nadav
On Sat, Feb 27, 2021 at 4:02 AM Christian Decker <decker.christ...@gmail.com>
wrote:
> > The `!(a && b && ...)` can be converted to a reversal of the payment.
> > The individual `!BUYER` is just the buyer choosing not to claim the
> > seller->buyer direction, and the individual `!ESCROW` is just the
> > escrow choosing not to reveal its temporary scalar for this payment.
> > And any products (i.e. `&&`) are trivially implemented in PTLCs as
> > trivial scalar and point addition.
> >
> > So it may actually be possible to express *any* Boolean logic, by the
> > use of reversal payments and "option not to release scalar", both of
> > which implement the NOT gate needed for the above. Boolean logic is a
> > fairly powerful, non-Turing-complete, and consistent programming
> > language, and if we can actually implement any kind of Boolean logic
> > with a set of payments in various directions and Barrier Escrows we
> > can enable some fairly complex use-cases..
>
> This got me thinking about my first year logic course and functional
> completeness [1], and it it trivial to prove that any boolean logic can
> be expressed by this construction. We can trivially build a functionally
> complete set by just constructing a NAND, a NOR, or {AND, NOT}, all of
> which you've already done in your prior mails.
>
> The resulting expressions may not be particularly nice, and result in a
> multitude of payments going back and forth between the participants to
> represent that logic, but it is possible. So the problem should now
> simply be reduced to finding a minimal representation for a given
> expression, which then minimizes the funds committed to a particular
> instance of the expression.
>
> Cheers,
> Christian
>
> [1] https://en.wikipedia.org/wiki/Functional_completeness
>
_______________________________________________
Lightning-dev mailing list
Lightning-dev@lists.linuxfoundation.org
https://lists.linuxfoundation.org/mailman/listinfo/lightning-dev
