Re: Proofs as programs

Hi,
In the below * is modus ponens, not composition.
For example B and B' are interchangeable.
B' = C*B
B = C*B'
What are C, B and B':
C: ((a->(b->c))->(b->(a->c))))
B: ((b->c)->((a->b)->(a->c))))
B': ((a->b)->((b->c)->(a->c)))
So there is not only the calculus based on BCI,
producing hilbert style proofs in affine logic.
but there is also the calculus based on B'CI.
Bye
P.S.: The Lafont & Girard paper shows a calculus
using B', B' is the composition operator of
categorical logics.
Julio Di Egidio schrieb:

On 17/12/2024 20:59, Mild Shock wrote:

Julio Di Egidio schrieb:

Sounds good?  Anything else? :)

5. Linear (BCI) and affine (BCK) combinatory logic
But I guess there are other ones as well?

 The RISK guy doesn't care about the million variants and inflorescences and accessories: to begin with, try and give some actual *substance* to your system.
 Here is some historical intro to the problem I am hinting at:
<https://plato.stanford.edu/entries/intuitionistic-logic-development/objections.html>   -Julio