Hi,

Create a proof search in Combinatory Logic,
that finds a Combinator Expression as proof
for a given formula in propositional logic.

The propositional logic can do with
implication only, and it should be Linear Logic.
French logician Jean-Yves Girard is credited

with Linear Logic, and since we have implication
logic only, the Logic will be also affine, i.e.
it will have no contraction, which makes

it special towards certain paradoxes.

Bye

Mild Shock schrieb:

Hi,

Draw a Colored ASCII Christams tree with Prolog.

Bye

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Hi,

Create a proof search in Simple Types,
that finds Lambda Expressions as proof,
for a given formula in propositional logic.

The logic is the same as in Weekend 2.

Bye

Mild Shock schrieb:

Hi,

Create a proof search in Combinatory Logic,
that finds a Combinator Expression as proof
for a given formula in propositional logic.

The propositional logic can do with
implication only, and it should be Linear Logic.
French logician Jean-Yves Girard is credited

with Linear Logic, and since we have implication
logic only, the Logic will be also affine, i.e.
it will have no contraction, which makes

it special towards certain paradoxes.

Bye

Mild Shock schrieb:

Hi,

Draw a Colored ASCII Christams tree with Prolog.

Bye

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 14/12/2024 22:13, Mild Shock wrote:

Create a proof search in Simple Types,
that finds Lambda Expressions as proof,
for a given formula in propositional logic.

Thinking about it:

Either by hand or with a 'solve', we/I [*] go from a Goal to a Proof
(proof tree). And, by Curry-Howard, that is (already!) our Type and
witnessing Term, i.e. our Proof is a program whose type is the Goal.
Indeed, we also already find type-checking: of a Proof against the Goal
it alleges to be a proof of.

What program does the Proof represent? If a Goal is of the form `G=>Z`,
where `G` is the context (some collection of Formulas as hypotheses),
and Formula `Z` is the conclusion, we interpret a Goal as a function
from the hypotheses to the conclusion.

To execute a Proof we need a "machine", namely, a function 'eval' that
takes the Proof as well as witnessing Terms for each hypothesis, and
returns a Term witnessing the conclusion. (Which also requires a system
of Terms: but I am not yet sure about the details...)

More than that, we can 'compile' the Proof to some target language (the system's host language being the first candidate), to produce a function
in the target language that is like 'eval' except specialized to the
given Proof as well as to as many hypothesis Terms as can be fixed...

Sounds good? Anything else? :)

-Julio

[*] See <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11#file-gentzen-pl>

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 17/12/2024 16:41, Julio Di Egidio wrote:

we interpret a Goal as a function
from the hypotheses to the conclusion.

Should read: as the type of functions from the hypotheses to the conclusion.

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Hi,

For a combinatory logic there is a hint here:

5. Linear (BCI) and affine (BCK) combinatory logic https://ncatlab.org/nlab/show/combinatory+logic#LinearAndAffine

But I guess there are other ones as well?

Bye

P.S.: I didn't verfy whether BCK and BCI are really
affine and linear. They write combinator I is also
definable as CKK, this would give an embedding of affine

into linear. But possibly not vice versa? Can we show
all these things via Prolog?

Julio Di Egidio schrieb:

Sounds good?  Anything else? :)

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Hi,

Some other ones are here:

Linear Logic and Lazy Computation
J. Y. Girard and Y. Lafont - TAPSOFT '87 https://www.researchgate.net/publication/226363607

But they have also other connectives, not only implication.

Bye

Mild Shock schrieb:

Hi,

For a combinatory logic there is a hint here:

5. Linear (BCI) and affine (BCK) combinatory logic https://ncatlab.org/nlab/show/combinatory+logic#LinearAndAffine

But I guess there are other ones as well?

Bye

P.S.: I didn't verfy whether BCK and BCI are really
affine and linear. They write combinator I is also
definable as CKK, this would give an embedding of affine

into linear. But possibly not vice versa? Can we show
all these things via Prolog?

Julio Di Egidio schrieb:

Sounds good?  Anything else? :)

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

No paywall here:

https://link.springer.com/content/pdf/10.1007%2FBFb0014972.pdfMild Shock schrieb:

Hi,

Some other ones are here:

Linear Logic and Lazy Computation
J. Y. Girard and Y. Lafont - TAPSOFT '87 https://www.researchgate.net/publication/226363607

But they have also other connectives, not only implication.

Bye

Mild Shock schrieb:

Hi,

For a combinatory logic there is a hint here:

5. Linear (BCI) and affine (BCK) combinatory logic
https://ncatlab.org/nlab/show/combinatory+logic#LinearAndAffine

But I guess there are other ones as well?

Bye

P.S.: I didn't verfy whether BCK and BCI are really
affine and linear. They write combinator I is also
definable as CKK, this would give an embedding of affine

into linear. But possibly not vice versa? Can we show
all these things via Prolog?

Julio Di Egidio schrieb:

Sounds good?  Anything else? :)

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Hi,

No paywall here:

Linear Logic and Lazy Computation
J. Y. Girard and Y. Lafont - TAPSOFT '87 https://link.springer.com/content/pdf/10.1007%2FBFb0014972.pdf

Bye

Mild Shock schrieb:

Hi,

Some other ones are here:

Linear Logic and Lazy Computation
J. Y. Girard and Y. Lafont - TAPSOFT '87 https://www.researchgate.net/publication/226363607

But they have also other connectives, not only implication.

Bye

Mild Shock schrieb:

Hi,

For a combinatory logic there is a hint here:

5. Linear (BCI) and affine (BCK) combinatory logic
https://ncatlab.org/nlab/show/combinatory+logic#LinearAndAffine

But I guess there are other ones as well?

Bye

P.S.: I didn't verfy whether BCK and BCI are really
affine and linear. They write combinator I is also
definable as CKK, this would give an embedding of affine

into linear. But possibly not vice versa? Can we show
all these things via Prolog?

Julio Di Egidio schrieb:

Sounds good?  Anything else? :)

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Hi,

The advent of logic tasks are not philosophical,
they directly ask for a calculus aka proof search
in Prolog. You could add some philosophical notes

to the resulting Prolog code.

Advent of Logic 2024: Weekend 2
Create a proof search in Combinatory Logic,
that finds a Combinator Expression as proof
for a given formula in propositional logic.

I have such a Prolog code already. Its relatively
easy to program. But I am hesitant to publish it,
still looking for BCI logic test cases.

Actually this paper could come handy:

BCK and BCI Logics, Condensed Detachment and the 2-Property
J. ROGER HINDLEY - Notre Dame Journal of Formal Logic
Volume 34, Number 2, Spring 1993 https://projecteuclid.org/journals/notre-dame-journal-of-formal-logic/volume-34/issue-2/BCK-and-BCI-logics-condensed-detachment-and-the-2-property/10.1305/ndjfl/1093634655.pdf

It has a section with a few test cases, such
as proving this formula:

a -> ((a -> b) -> b)

Bye

Mild Shock schrieb:

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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 18/12/2024 08:43, Mild Shock wrote:

The advent of logic tasks are not philosophical,
they directly ask for a calculus aka proof search
in Prolog. You could add some philosophical notes
to the resulting Prolog code.

"Philosophy" as in not being a vacuous dumb fuck? I hope.

I was asking if my work would qualify for your challenge, in fact what
the challenge even is, since you cannot write a problem statement that
is one.

When you have missed that point, I have pointed out that accessorized
system variant 1765234 is utterly uninteresting when pure system 0 is
already a difficult foundational then coding problem otherwise a cheat.

But don't take my word for it.

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

The challenge is this here:

Mild Shock schrieb:

Advent of Logic 2024: Weekend 2
Create a *proof search* in Combinatory Logic,
that finds a Combinator Expression as proof
for a given formula in propositional logic.

The propositional logic can do with
implication only, and it should be *Linear Logic*.
French logician Jean-Yves Girard is credited

with Linear Logic, and since we have implication
logic only, the Logic will be also *affine*, i.e.
it will have no contraction, which makes

it special towards certain paradoxes.

As a test case, you could show for example a proof of:

(a -> ((a -> b) -> b))

But you find more formulas as test cases here:

BCK and BCI Logics, Condensed Detachment and the 2-Property
J. ROGER HINDLEY - Notre Dame Journal of Formal Logic
Volume 34, Number 2, Spring 1993 https://projecteuclid.org/journals/notre-dame-journal-of-formal-logic/volume-34/issue-2/BCK-and-BCI-logics-condensed-detachment-and-the-2-property/10.1305/ndjfl/1093634655.pdf

Section 3.6.1 and 3.6.2 are test cases.

Julio Di Egidio schrieb:

On 18/12/2024 08:43, Mild Shock wrote:

The advent of logic tasks are not philosophical,
they directly ask for a calculus aka proof search
in Prolog. You could add some philosophical notes
to the resulting Prolog code.

"Philosophy" as in not being a vacuous dumb fuck?  I hope.

I was asking if my work would qualify for your challenge, in fact what
the challenge even is, since you cannot write a problem statement that
is one.

When you have missed that point, I have pointed out that accessorized
system variant 1765234 is utterly uninteresting when pure system 0 is
already a difficult foundational then coding problem otherwise a cheat.

But don't take my word for it.

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 18/12/2024 15:30, Mild Shock wrote:

Maybe your work qualifies for Weekend 3.

In fact, I have replied to the WE3 announcement.

I don't know yet. You have to tell us. Do
you think it implements a Natural Deduction
with Simple Types proof extraction?

It implements "affine intuitionistic propositional logic", and I am
getting to evaluation/compilation which is the functional side (more
details in my initial reply): so, sure, I even classify my reduction
rules as intros vs elims...

What is the deadline? I don't know what WE is 3.

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 17/12/2024 16:41, Julio Di Egidio wrote:

On 14/12/2024 22:13, Mild Shock wrote:

Create a proof search in Simple Types,
that finds Lambda Expressions as proof,
for a given formula in propositional logic.

Thinking about it:

Either by hand or with a 'solve', we/I [*] go from a Goal to a Proof
(proof tree).  And, by Curry-Howard, that is (already!) our Type and witnessing Term, i.e. our Proof is a program whose type is the Goal.
Indeed, we also already find type-checking: of a Proof against the Goal
it alleges to be a proof of.

<snip>

My interpretation might be unorthodox, anyway here is concretely what I
am doing (a far better approximation that is): <https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Syntax-directed_rule_system>

So yeah, my system definitely qualifies, assuming I meet a deadline that remains a mystery to this point - I guess that's the main challenge.

<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11#file-gentzen-pl>

Meanwhile, kindly, for your records:

```
?- case(codile, LT, G), prove(LT, G, Ps), print_ps(Ps). % v30-alpha
[
orE(0)
[
orIL
impE(2)
[
init(0)
]
[
init(0)
]
]
[
orIR
impE(1)
[
init(0)
]
[
init(0)
]
]
]
LT = pos,
G = ([(p->q),(r->s),p\/r]=>q\/s),
Ps = [orE(0),[orIL,impE(2),[init(0)],[init(0)]],
[orIR,impE(1),[init(0)],[init(0)]]] .

% 3 more solutions...
```

Have fun,

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Hi,

I even wonder why you talk about Proofs as Programs.
Your calculus is not suitable. Proofs as Progams
usually uses Natural Deduction. There are very few

systems that use Sequent Calculus. Well if your rules
here were really impI and impE:

% (C=>X->Y) --> [(C,X=>Y)]
reduction(impI, (C=>X->Y), [[X|C]=>Y], []).

% (C,X->Y=>Z) --> [(C=>X),(C,Y=>Z)]
reduction(impE, (C0=>Z), [C=>X,[Y|C]=>Z], [H]) :-
use_hyp((_->_), C0, (X->Y), C, H).

https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11

Then you would have solved Weekend 3 already for long.
Because if they really were impI and impE you
could easily extract lambda expression. After all

Curry Howard has these two impI and impE rules:

Γ, α ⊢ β
-------------- (→I)
Γ ⊢ α → β

Γ ⊢ α → β Γ ⊢ α
--------------------- (→E)
Γ ⊢ β

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Intuitionistic_Natural_deduction_and_typed_lambda_calculus

But your Prolog obviously doesn't realize
the two rules (→I) and (→E).

The rule impE is wrong. Also you cannot use
reduction technique for Natural Deduction, because
the (→E) rule invents a new formula β in backward

chaining. So it wouldn't be a proper reduction,
when it invents something. The formulas get sometimes
in a first phase larger and not necessarey

smaller in Natural Deduction. So you would need to
deploy a similar search as in Weekend 2.
The BCI search.

Julio Di Egidio schrieb:

On 14/12/2024 22:13, Mild Shock wrote:

Create a proof search in Simple Types,
that finds Lambda Expressions as proof,
for a given formula in propositional logic.

Thinking about it:

Either by hand or with a 'solve', we/I [*] go from a Goal to a Proof
(proof tree).  And, by Curry-Howard, that is (already!) our Type and witnessing Term, i.e. our Proof is a program whose type is the Goal.
Indeed, we also already find type-checking: of a Proof against the Goal
it alleges to be a proof of.

What program does the Proof represent?  If a Goal is of the form `G=>Z`, where `G` is the context (some collection of Formulas as hypotheses),
and Formula `Z` is the conclusion, we interpret a Goal as a function
from the hypotheses to the conclusion.

To execute a Proof we need a "machine", namely, a function 'eval' that
takes the Proof as well as witnessing Terms for each hypothesis, and
returns a Term witnessing the conclusion.  (Which also requires a system
of Terms: but I am not yet sure about the details...)

More than that, we can 'compile' the Proof to some target language (the system's host language being the first candidate), to produce a function
in the target language that is like 'eval' except specialized to the
given Proof as well as to as many hypothesis Terms as can be fixed...

Sounds good?  Anything else?  :)

-Julio

[*] See <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11#file-gentzen-pl>

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 19/12/2024 18:40, Julio Di Egidio wrote:

My interpretation might be unorthodox,
anyway here is concretely what I am doing
(a far better approximation that is): <https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Syntax-directed_rule_system>

That is, Hindley-Milner upside down:
a *closed* universe with Prop on top...

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Its different from yours. Yours has, it is
wrongly labled should be impL:

% (C,X->Y=>Z) --> [(C=>X),(C,Y=>Z)] /* A */
reduction(impE, (C0=>Z), [C=>X,[Y|C]=>Z], [H]) :-
use_hyp((_->_), C0, (X->Y), C, H).

On the other hand Hindley–Milner has [App],
which is the real impE:

% (C=>Y) --> [(C=>X->Y),(C=>X)] /* B */ https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Syntax-directed_rule_system

/* A */ and /* B */ are different:

/* A */ Belongs to Sequent Calculus
in Gentzens Paper the Systems LJ and LK

/* B */ Belongs to Natural Deduction,
in Gentzens Paper the Systems NJ and NK

Algorithm W is what a Prolog interpreter would
do, when the Proof Term is given and when we
want to find the Principal Type.

For Weekend 3 the task is different, the Type
is given and we want to find the Proof Term.

Julio Di Egidio schrieb:

On 19/12/2024 18:40, Julio Di Egidio wrote:

My interpretation might be unorthodox, anyway here is concretely what
I am doing (a far better approximation that is):
<https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Syntax-directed_rule_system>

That is, Hindley-Milner upside down:
a *closed* universe with Prop on top...

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Hi,

The Task of Weekend 2 and Weekend 3 is called
the Inhabitation Problem. Its different from
Syntax-directed rule system.

https://en.wikipedia.org/wiki/Type_inhabitation

In the solution to Weekend 2 you see how
Types can be inhabitated by Combinatorial
Expressions. The code is here:

/* vanilla interpreter with typeof/2 counting */
% search(+Goal, +Integer, -Integer)
search(true, N, N).
search((A,B), N, M) :-
search(A, N, H),
search(B, H, M).
search(typeof(P, T), N, M) :- N>0, H is N-1,
clause(typeof(P, T), B),
search(B, H, M).
search(unify_with_occurs_check(A,B), N, N) :-
unify_with_occurs_check(A,B). https://gist.github.com/Jean-Luc-Picard-2021/bc829e6c002b955a51a49ae3bf384c72

It uses a form of iterative deepening,
and finds shortes Combinatorial
Expressions first.

You can apply the same search in Weekend 3,
and find Lambda Expressions instead of
Combinatorial Expressions.

But Weekend 3 should be Natural Deduction
and not Sequent Calculus. You could solve
Sequent Calculus as Weekend 4.

Mild Shock schrieb:

Its different from yours. Yours has, it is
wrongly labled should be impL:

% (C,X->Y=>Z) --> [(C=>X),(C,Y=>Z)]    /* A */
reduction(impE, (C0=>Z), [C=>X,[Y|C]=>Z], [H]) :-
use_hyp((_->_), C0, (X->Y), C, H).

On the other hand Hindley–Milner has [App],
which is the real impE:

% (C=>Y) --> [(C=>X->Y),(C=>X)]    /* B */ https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Syntax-directed_rule_system

/* A */ and /* B */ are different:

/* A */ Belongs to Sequent Calculus
in Gentzens Paper the Systems LJ and LK

/* B */ Belongs to Natural Deduction,
in Gentzens Paper the Systems NJ and NK

Algorithm W is what a Prolog interpreter would
do, when the Proof Term is given and when we
want to find the Principal Type.

For Weekend 3 the task is different, the Type
is given and we want to find the Proof Term.

Julio Di Egidio schrieb:

On 19/12/2024 18:40, Julio Di Egidio wrote:

My interpretation might be unorthodox, anyway here is concretely what
I am doing (a far better approximation that is):
<https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Syntax-directed_rule_system>

That is, Hindley-Milner upside down:
a *closed* universe with Prop on top...

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 23/12/2024 00:51, Mild Shock wrote:

Its different from yours.

Hallelujah.

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Hi,

Now that Christmas is over, are you excited for the new year?

Here is the task for Weekend 4:

- Do the same as for Weekend 2 and Weekend 3
for a relevant logic.

This would complete the picture, since we would have:

Logic Weakening Contraction
Minimal Yes Yes
Relevant No Yes
Affine Yes No
Linear No No

Bye

Mild Shock schrieb:

Hi,

Create a proof search in Simple Types,
that finds Lambda Expressions as proof,
for a given formula in propositional logic.

The logic is the same as in Weekend 2.

Bye

Mild Shock schrieb:

Hi,

Create a proof search in Combinatory Logic,
that finds a Combinator Expression as proof
for a given formula in propositional logic.

The propositional logic can do with
implication only, and it should be Linear Logic.
French logician Jean-Yves Girard is credited

with Linear Logic, and since we have implication
logic only, the Logic will be also affine, i.e.
it will have no contraction, which makes

it special towards certain paradoxes.

Bye

Mild Shock schrieb:

Hi,

Draw a Colored ASCII Christams tree with Prolog.

Bye

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)