Hi,

Draw a Colored ASCII Christams tree with Prolog.

Bye

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

Specification:


Weekend 2:
-----------
- Input = Atom % Propositional variable
| Input -> Input % Implication

- Output = B % B Axiom Schema
| C % C Axiom Schema
| I % I Axiom Schema
| (Output Output) % Modus Ponens

Weekend 3:
-----------
- Input = Atom % Propositional variable
| Input -> Input % Implication

- Output = Variable % Repetition
| λVariable.Output % Assumption & Detachment
| (Output Output) % Modus Ponens


Deadline:

24. December 2024

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

Its quite intersting that Affine Logic can
be measured by the realization of this output:

- Output = Variable % Repetition

Its seems to me that in Affine Logic a variable
is only allowed to occur in a Repetition at most
once, it seems also to me that each variable

must be also repeated at least once. So that
variables are repreated exactly once.

Here is a counter example with too many repetitions,
this would not be a valid output for weekend 3,
since it cannot be converted into the output of weekend 2:

λx:A->A.λy:A.(x (x y)) : ((A -> A) -> (A -> A))

And her is a counter example with too few repetitions,
equally well it cannot be converted to a BCI expression.

λx:A.λy:B.x : (A -> (B -> A))

I tried it heuristically, Affine Logic can indeed not
prove (A -> (B -> A)). Don't know yet how to show it
rigorously, this would need some model theory.

Mild Shock schrieb:

Specification:

Weekend 2:
-----------
- Input = Atom            % Propositional variable
        | Input -> Input  % Implication

- Output = B               % B Axiom Schema
         | C               % C Axiom Schema
         | I               % I Axiom Schema
         | (Output Output) % Modus Ponens

Weekend 3:
-----------
- Input = Atom            % Propositional variable
        | Input -> Input  % Implication

- Output = Variable         % Repetition
         | λVariable.Output % Assumption & Detachment
         | (Output Output)  % Modus Ponens

Deadline:

24. December 2024

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

As a warmup I started with a subintuitionistic logic:

https://gist.github.com/Jean-Luc-Picard-2021/bc829e6c002b955a51a49ae3bf384c72#file-minimal-p

With these test cases:

/* 4 positive test cases */

% ?- between(1,13,N), search(typeof(X, ((a->a)->(a->a))), N, 0).
% N = 3,
% X = s*k .

% ?- between(1,13,N), search(typeof(X, (a->((a->b)->b))), N, 0).
% N = 13,
% X = s*(k*(s*(s*k*k)))*k .

% ?- between(1,13,N), search(typeof(X, (a->(b->a))), N, 0).
% N = 1,
% X = k .

% ?- between(1,13,N), search(typeof(X, ((a->(a->b))->(a->b))), N, 0).
% N = 7,
% X = s*s*(s*k) .

And then I made the required substructural logic:

https://gist.github.com/Jean-Luc-Picard-2021/bc829e6c002b955a51a49ae3bf384c72#file-affine-p

With these test cases:

/* 2 positive test cases */

% ?- between(1,13,N), search(typeof(X, ((a->a)->(a->a))), N, 0).
% N = 1,
% X = i .

% ?- between(1,13,N), search(typeof(X, (a->((a->b)->b))), N, 0).
% N = 3,
% X = c*i .

/* 2 negative test cases */

% ?- between(1,13,N), search(typeof(X, (a->(b->a))), N, 0).
% false.

% ?- between(1,13,N), search(typeof(X, ((a->(a->b))->(a->b))), N, 0).
% false.

Mild Shock schrieb:

Its quite intersting that Affine Logic can
be measured by the realization of this output:

- Output = Variable         % Repetition

Its seems to me that in Affine Logic a variable
is only allowed to occur in a Repetition at most
once, it seems also to me that each variable

must be also repeated at least once. So that
variables are repreated exactly once.

Here is a counter example with too many repetitions,
this would not be a valid output for weekend 3,
since it cannot be converted into the output of weekend 2:

λx:A->A.λy:A.(x (x y))   :  ((A -> A) -> (A -> A))

And her is a counter example with too few repetitions,
equally well it cannot be converted to a BCI expression.

λx:A.λy:B.x : (A -> (B -> A))

I tried it heuristically, Affine Logic can indeed not
prove (A -> (B -> A)). Don't know yet how to show it
rigorously, this would need some model theory.

Mild Shock schrieb:

Specification:


Weekend 2:
-----------
- Input = Atom            % Propositional variable
         | Input -> Input  % Implication

- Output = B               % B Axiom Schema
          | C               % C Axiom Schema
          | I               % I Axiom Schema
          | (Output Output) % Modus Ponens

Weekend 3:
-----------
- Input = Atom            % Propositional variable
         | Input -> Input  % Implication

- Output = Variable         % Repetition
          | λVariable.Output % Assumption & Detachment
          | (Output Output)  % Modus Ponens


Deadline:

24. December 2024

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

On 20/12/2024 02:48, Mild Shock wrote:

Its quite intersting that Affine Logic can
be measured by the realization of this output:

- Output = Variable         % Repetition

Though, can it? (More below.)

λx:A.λy:B.x : (A -> (B -> A))
I tried it heuristically, Affine Logic can indeed not
prove (A -> (B -> A)). Don't know yet how to show it
rigorously, this would need some model theory.

That is simply wrong, affine logic can of course prove a statement
where, after the intros, hypothesis 1 is used once and hypothesis 2 is
not used at all. That wouldn't be valid for linear logic (in the sense
still of a substructural logic), as we are not using all hypothesis.

As to how that relates to the lambda calculus side I still don't know,
but I find significant that you says Repetition while I (substructural
logic) says Use...

-Julio

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

Hi,

Friendly Reminder that the Deadline 24. December 2024
is approaching. Please be aware that Weekend 3 asks for
Natural Deduction, where (E⊃) and Modus Ponens are synonymous:

/* Scope of Weekend 3 */

C, X ⊢ Y
-------------- (I⊃)
C ⊢ X ⊃ Y

C ⊢ X C ⊢ X ⊃ Y
--------------------- (E⊃) /* Also known as Modus Ponens */
C ⊢ Y


Simply Types and its Curry Howard is primarily defined
for Natural Deduction. Extracting Lambda Experessions
from Non-Natural Deduction is a little bit more complicated.

So Weekend 3 is NOT for Sequent Calculus:

/* Not Scope of Weekend 3 */

C, X ⊢ Y
-------------- (R⊃)
C ⊢ X ⊃ Y

C ⊢ X C, Y ⊢ Z
--------------------- (L⊃)
C, X ⊃ Y ⊢ Z

Bye

Mild Shock schrieb:

Specification:

Weekend 2:
-----------
- Input = Atom            % Propositional variable
        | Input -> Input  % Implication

- Output = B               % B Axiom Schema
         | C               % C Axiom Schema
         | I               % I Axiom Schema
         | (Output Output) % Modus Ponens

Weekend 3:
-----------
- Input = Atom            % Propositional variable
        | Input -> Input  % Implication

- Output = Variable         % Repetition
         | λVariable.Output % Assumption & Detachment
         | (Output Output)  % Modus Ponens

Deadline:

24. December 2024

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

Ok, I made a solution for Weekend 3,
first I made minimal logic. I opted for
Lambda Expressions with de Brujin indexes:

/* 4 positive test cases */

% ?- between(1,13,N), search(typeof(X, [], ((a->a)->(a->a))), N, 0).
% N = 2,
% X = lam((a->a), 0) .

% ?- between(1,13,N), search(typeof(X, [], (a->((a->b)->b))), N, 0).
% N = 5,
% X = lam(a, lam((a->b), 0*1)) .

% ?- between(1,13,N), search(typeof(X, [], (a->(b->a))), N, 0).
% N = 3,
% X = lam(a, lam(b, 1)) .

% ?- between(1,13,N), search(typeof(X, [], ((a->(a->b))->(a->b))), N, 0).
% N = 7,
% X = lam((a->a->b), lam(a, 1*0*0)) .

For example the 2nd solution with de Brujin indexs
can be read without de Brujin indexes as follows:

λx:a.λy:(a->b).(y x) : (a->((a->b)->b))

https://gist.github.com/Jean-Luc-Picard-2021/db6f71f66781838c98ee8b828eb5b9c2#file-minimal-p

Mild Shock schrieb:

Hi,

Friendly Reminder that the Deadline 24. December 2024
is approaching. Please be aware that Weekend 3 asks for
Natural Deduction, where (E⊃) and Modus Ponens are synonymous:

/* Scope of Weekend 3 */

  C, X  ⊢  Y
-------------- (I⊃)
  C ⊢ X ⊃ Y

  C ⊢ X    C ⊢ X ⊃ Y
--------------------- (E⊃) /* Also known as Modus Ponens */
       C ⊢ Y

Simply Types and its Curry Howard is primarily defined
for Natural Deduction. Extracting Lambda Experessions
from Non-Natural Deduction is a little bit more complicated.

So Weekend 3 is NOT for Sequent Calculus:

/* Not Scope of Weekend 3 */

  C, X  ⊢  Y
-------------- (R⊃)
  C ⊢ X ⊃ Y

  C ⊢ X    C, Y ⊢ Z
--------------------- (L⊃)
    C, X ⊃ Y ⊢ Z

Bye

Mild Shock schrieb:

Specification:


Weekend 2:
-----------
- Input = Atom            % Propositional variable
         | Input -> Input  % Implication

- Output = B               % B Axiom Schema
          | C               % C Axiom Schema
          | I               % I Axiom Schema
          | (Output Output) % Modus Ponens

Weekend 3:
-----------
- Input = Atom            % Propositional variable
         | Input -> Input  % Implication

- Output = Variable         % Repetition
          | λVariable.Output % Assumption & Detachment
          | (Output Output)  % Modus Ponens


Deadline:

24. December 2024

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

I skipped doing an affine logic. But one can derive
it from the linear logic. So I made a linear logic.
It is derived from the minimal logic but typeof

as a different signatur:

/* Minimal Logic */
G |- M : t /* typeof(M, G, t) */

/* Linear Logic
G |- M : t | G' /* typeof(M, G, G', t) */

The updated context G' does a tracking and sees to it
that every assumption is only use once. An assumption
has initially the flag 0 and when it was used it has

the flag 1. There are two places in the code where
this is used:

/* Implication Intro */
typeof(lam(A, Y), L, R, (A -> B)) :-
typeof(Y, [A-0|L], [A-1|R], B).
/* Axiom */
typeof(K, L, R, B) :-
nth0(K, L, A-0, H),
unify_with_occurs_check(A, B),
nth0(K, R, A-1, H).

Its not yet extremly tested. And its not widely known,
since most presentations are Sequent Calculus and not
Natural Deduction. I only found one paper:

Introduction to linear logic - Emmanuel Beffara
Table 6: Intuitionistic linear logic as natural deduction https://hal.science/cel-01144229

Mild Shock schrieb:

Ok, I made a solution for Weekend 3,
first I made minimal logic. I opted for
Lambda Expressions with de Brujin indexes:

/* 4 positive test cases */

% ?- between(1,13,N), search(typeof(X, [], ((a->a)->(a->a))), N, 0).
% N = 2,
% X = lam((a->a), 0) .

% ?- between(1,13,N), search(typeof(X, [], (a->((a->b)->b))), N, 0).
% N = 5,
% X = lam(a, lam((a->b), 0*1)) .

% ?- between(1,13,N), search(typeof(X, [], (a->(b->a))), N, 0).
% N = 3,
% X = lam(a, lam(b, 1)) .

% ?- between(1,13,N), search(typeof(X, [], ((a->(a->b))->(a->b))), N, 0).
% N = 7,
% X = lam((a->a->b), lam(a, 1*0*0)) .

For example the 2nd solution with de Brujin indexs
can be read without de Brujin indexes as follows:

λx:a.λy:(a->b).(y x)    :    (a->((a->b)->b))

https://gist.github.com/Jean-Luc-Picard-2021/db6f71f66781838c98ee8b828eb5b9c2#file-minimal-p

Mild Shock schrieb:

Hi,

Friendly Reminder that the Deadline 24. December 2024
is approaching. Please be aware that Weekend 3 asks for
Natural Deduction, where (E⊃) and Modus Ponens are synonymous:

/* Scope of Weekend 3 */

   C, X  ⊢  Y
-------------- (I⊃)
   C ⊢ X ⊃ Y

   C ⊢ X    C ⊢ X ⊃ Y
--------------------- (E⊃) /* Also known as Modus Ponens */
        C ⊢ Y


Simply Types and its Curry Howard is primarily defined
for Natural Deduction. Extracting Lambda Experessions
from Non-Natural Deduction is a little bit more complicated.

So Weekend 3 is NOT for Sequent Calculus:

/* Not Scope of Weekend 3 */

   C, X  ⊢  Y
-------------- (R⊃)
   C ⊢ X ⊃ Y

   C ⊢ X    C, Y ⊢ Z
--------------------- (L⊃)
     C, X ⊃ Y ⊢ Z

Bye

Mild Shock schrieb:

Specification:


Weekend 2:
-----------
- Input = Atom            % Propositional variable
         | Input -> Input  % Implication

- Output = B               % B Axiom Schema
          | C               % C Axiom Schema
          | I               % I Axiom Schema
          | (Output Output) % Modus Ponens

Weekend 3:
-----------
- Input = Atom            % Propositional variable
         | Input -> Input  % Implication

- Output = Variable         % Repetition
          | λVariable.Output % Assumption & Detachment
          | (Output Output)  % Modus Ponens


Deadline:

24. December 2024

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

The source code is here:

https://gist.github.com/Jean-Luc-Picard-2021/db6f71f66781838c98ee8b828eb5b9c2#file-linear-p

And some testing is here:

/* 2 positive test cases */

% ?- between(1,13,N), search(typeof(X, [], [], ((a->a)->(a->a))), N, 0).
% N = 2,
% X = lam((a->a), 0) .

% ?- between(1,13,N), search(typeof(X, [], [], (a->((a->b)->b))), N, 0).
% N = 5,
% X = lam(a, lam((a->b), 0*1)) .

/* 2 negative test cases */

% ?- between(1,13,N), search(typeof(X, [], [], (a->(b->a))), N, 0).
% false.

% ?- between(1,13,N), search(typeof(X, [], [], ((a->(a->b))->(a->b))),
N, 0).
% false.

Mild Shock schrieb:

I skipped doing an affine logic. But one can derive
it from the linear logic. So I made a linear logic.
It is derived from the minimal logic but typeof

as a different signatur:

/* Minimal Logic */
G |- M : t              /* typeof(M, G, t) */

/* Linear Logic
G |- M : t | G'         /* typeof(M, G, G', t) */

The updated context G' does a tracking and sees to it
that every assumption is only use once. An assumption
has initially the flag 0 and when it was used it has

the flag 1. There are two places in the code where
this is used:

/* Implication Intro */
typeof(lam(A, Y), L, R, (A -> B)) :-
   typeof(Y, [A-0|L], [A-1|R], B).
/* Axiom */
typeof(K, L, R, B) :-
   nth0(K, L, A-0, H),
   unify_with_occurs_check(A, B),
   nth0(K, R, A-1, H).

Its not yet extremly tested. And its not widely known,
since most presentations are Sequent Calculus and not
Natural Deduction. I only found one paper:

Introduction to linear logic - Emmanuel Beffara
Table 6: Intuitionistic linear logic as natural deduction https://hal.science/cel-01144229

Mild Shock schrieb:

Ok, I made a solution for Weekend 3,
first I made minimal logic. I opted for
Lambda Expressions with de Brujin indexes:

/* 4 positive test cases */

% ?- between(1,13,N), search(typeof(X, [], ((a->a)->(a->a))), N, 0).
% N = 2,
% X = lam((a->a), 0) .

% ?- between(1,13,N), search(typeof(X, [], (a->((a->b)->b))), N, 0).
% N = 5,
% X = lam(a, lam((a->b), 0*1)) .

% ?- between(1,13,N), search(typeof(X, [], (a->(b->a))), N, 0).
% N = 3,
% X = lam(a, lam(b, 1)) .

% ?- between(1,13,N), search(typeof(X, [], ((a->(a->b))->(a->b))), N, 0).
% N = 7,
% X = lam((a->a->b), lam(a, 1*0*0)) .

For example the 2nd solution with de Brujin indexs
can be read without de Brujin indexes as follows:

λx:a.λy:(a->b).(y x)    :    (a->((a->b)->b))

https://gist.github.com/Jean-Luc-Picard-2021/db6f71f66781838c98ee8b828eb5b9c2#file-minimal-p


Mild Shock schrieb:

Hi,

Friendly Reminder that the Deadline 24. December 2024
is approaching. Please be aware that Weekend 3 asks for
Natural Deduction, where (E⊃) and Modus Ponens are synonymous:

/* Scope of Weekend 3 */

   C, X  ⊢  Y
-------------- (I⊃)
   C ⊢ X ⊃ Y

   C ⊢ X    C ⊢ X ⊃ Y
--------------------- (E⊃) /* Also known as Modus Ponens */
        C ⊢ Y


Simply Types and its Curry Howard is primarily defined
for Natural Deduction. Extracting Lambda Experessions
from Non-Natural Deduction is a little bit more complicated.

So Weekend 3 is NOT for Sequent Calculus:

/* Not Scope of Weekend 3 */

   C, X  ⊢  Y
-------------- (R⊃)
   C ⊢ X ⊃ Y

   C ⊢ X    C, Y ⊢ Z
--------------------- (L⊃)
     C, X ⊃ Y ⊢ Z

Bye

Mild Shock schrieb:

Specification:


Weekend 2:
-----------
- Input = Atom            % Propositional variable
         | Input -> Input  % Implication

- Output = B               % B Axiom Schema
          | C               % C Axiom Schema
          | I               % I Axiom Schema
          | (Output Output) % Modus Ponens

Weekend 3:
-----------
- Input = Atom            % Propositional variable
         | Input -> Input  % Implication

- Output = Variable         % Repetition
          | λVariable.Output % Assumption & Detachment
          | (Output Output)  % Modus Ponens


Deadline:

24. December 2024

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

Programming languages such as Vault, Rust, etc.. have
recently popularized substructural logics. Their type
systems share various forms of resource awareness.

Propositional substructural logics were already
discussed when Jan Łukasiewicz and Carew Arthur Meredith
met in 1947 in Dublin. We will investigate such logics
with the help of Prolog.

Links to Dogelog Notebooks that capture the proof finder
and the model finder are given at the end of the post.
We have practically automatized the work of a Logician
in the middle of the previous century.

We could determine proper inclusions relationships
among the examined Minimal, Affine, Relevant and
Linear logics.

See also:

Substructural Logics via Dogelog Player https://x.com/dogelogch/status/1880084983316115798

Substructural Logics via Dogelog Player
https://www.facebook.com/groups/dogelog

Mild Shock schrieb:

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

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