Hi,

There are some reduction techniques that more
or less work for natural deduction. But its
not so easy, you need Long Head Normal form

and stuff. But Prolog code, a description of it,
has been published for example here. Guess who
wrote the Prolog code paper?

August 1988
https://www.researchgate.net/publication/322069446

Its based on the original Howard paper which uses a
multi premisse rule. So its not a rule with a fixed
arity. Namely its this rule:

Γ ⊢ α1 .... Γ ⊢ αn
-----------------------------
Γ ⊢ α1→...αn→β ⊃ β

You can use the above for reduction. And it
has a Natural Deduction Flair. You can also related
the above rule to Sequent calculus.

Its quite a Christmas Miracle.

Bye

Mild Shock schrieb:

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

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)

Hi,

But it also explains why you need to apply the
Dragalin "Copying". If you would really implement:

Γ ⊢ α1 .... Γ ⊢ αn
-----------------------------
Γ, (β :- α1, .., αn) ⊢ β

The above could indicate that you remove the applied
rule (β :- α1, .., αn). But you might have subgoals
that need the rule again. So the Prolog-ish and

als the intuitionistic system has in fact:

Γ, γ ⊢ α1 .... Γ, γ ⊢ αn
-------------------------------
Γ, γ ⊢ β

Where γ = (β :- α1, .., αn). So we are in the mist
of Affine logic, which would probaly forbid the
use of the rule a second or third time.

Lets see whether we can solve Weekend 3.

Bye

Mild Shock schrieb:

Hi,

Corr.: Typo., This way its not Natural Deduction:

      Γ ⊢ α1    ....  Γ ⊢ αn
   -----------------------------
     Γ, α1 → ...  → αn → β ⊢ β

Only this way it would be Natural Deduction:

      Γ ⊢ α1    ....  Γ ⊢ αn
   -----------------------------
     Γ ⊢ (α1 → ...  → αn → β) → β

But lets stick to the first form. Interestingly the
multi-premisse rule is Prolog itself in disguise.
Just observe that we usually have for conjunction:

   α → (β → γ)  ==  α ∧ β → γ

So we can write the rule as:

      Γ ⊢ α1    ....  Γ ⊢ αn
   -----------------------------
     Γ,  α1 ∧  ... ∧ αn → β ⊢ β

Now use comman and Prolog implication and you can write it:

      Γ ⊢ α1    ....  Γ ⊢ αn
   -----------------------------
     Γ, (β :- α1, .., αn) ⊢ β

Thats basically the declarative reading,
reading ⊢ as "is true":

"The goal β is true if the subgoals ​α1, .., αn are all true."

Bye

Mild Shock schrieb:

Hi,sub

There are some reduction techniques that more
or less work for natural deduction. But its
not so easy, you need Long Head Normal form

and stuff. But Prolog code, a description of it,
has been published for example here. Guess who
wrote the Prolog code paper?

August 1988
https://www.researchgate.net/publication/322069446

Its based on the original Howard paper which uses a
multi premisse rule. So its not a rule with a fixed
arity. Namely its this rule:

     Γ ⊢ α1    ....  Γ ⊢ αn
  -----------------------------
    Γ, α1 → ...  → αn → β ⊢ β

You can use the above for reduction. And it
has a Natural Deduction Flair. You can also related
the above rule to Sequent calculus.

Its quite a Christmas Miracle.

Bye

Mild Shock schrieb:

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

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)

Hi,

Corr.: Typo., This way its not Natural Deduction:

Γ ⊢ α1 .... Γ ⊢ αn
-----------------------------
Γ, α1 → ... → αn → β ⊢ β

Only this way it would be Natural Deduction:

Γ ⊢ α1 .... Γ ⊢ αn
-----------------------------
Γ ⊢ (α1 → ... → αn → β) → β

But lets stick to the first form. Interestingly the
multi-premisse rule is Prolog itself in disguise.
Just observe that we usually have for conjunction:

α → (β → γ) == α ∧ β → γ

So we can write the rule as:

Γ ⊢ α1 .... Γ ⊢ αn
-----------------------------
Γ, α1 ∧ ... ∧ αn → β ⊢ β

Now use comman and Prolog implication and you can write it:

Γ ⊢ α1 .... Γ ⊢ αn
-----------------------------
Γ, (β :- α1, .., αn) ⊢ β

Thats basically the declarative reading,
reading ⊢ as "is true":

"The goal β is true if the subgoals ​α1, .., αn are all true."

Bye

Mild Shock schrieb:

Hi,sub

There are some reduction techniques that more
or less work for natural deduction. But its
not so easy, you need Long Head Normal form

and stuff. But Prolog code, a description of it,
has been published for example here. Guess who
wrote the Prolog code paper?

August 1988
https://www.researchgate.net/publication/322069446

Its based on the original Howard paper which uses a
multi premisse rule. So its not a rule with a fixed
arity. Namely its this rule:

    Γ ⊢ α1    ....  Γ ⊢ αn
 -----------------------------
  Γ, α1 → ... → αn → β ⊢ β

You can use the above for reduction. And it
has a Natural Deduction Flair. You can also related
the above rule to Sequent calculus.

Its quite a Christmas Miracle.

Bye

Mild Shock schrieb:

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

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)

Hi,

In Prolog using a rule again in the propositional
case usually leads to looping. Like here:

q.
r.
p :- q, p, r.

But in the non-propositional case its very
common and constitutes recursion:

append([],X,X).
append([X|Y],Z,[X|T]) :- append(Y,Z,T).

A query as follows:

?- append([1,2],[3],X).
X = [1,2,3]

Uses the 2nd rule of append/3 twice.

Bye

Mild Shock schrieb:

Hi,

But it also explains why you need to apply the
Dragalin "Copying". If you would really implement:

        Γ ⊢ α1    ....  Γ ⊢ αn
     -----------------------------
       Γ, (β :- α1, .., αn) ⊢ β

The above could indicate that you remove the applied
rule (β :- α1, .., αn). But you might have subgoals
that need the rule again. So the Prolog-ish and

als the intuitionistic system has in fact:

   Γ, γ ⊢ α1    ....  Γ, γ ⊢ αn
  -------------------------------
           Γ, γ ⊢ β

Where γ = (β :- α1, .., αn). So we are in the mist
of Affine logic, which would probaly forbid the
use of the rule a second or third time.

Lets see whether we can solve Weekend 3.

Bye

Mild Shock schrieb:

Hi,

Corr.: Typo., This way its not Natural Deduction:

;      Γ ⊢ α1    ....  Γ ⊢ αn
;   -----------------------------
;     Γ, α1 → ...  → αn → β ⊢ β

Only this way it would be Natural Deduction:

;      Γ ⊢ α1    ....  Γ ⊢ αn
;   -----------------------------
;     Γ ⊢ (α1 → ...  → αn → β) → β

But lets stick to the first form. Interestingly the
multi-premisse rule is Prolog itself in disguise.
Just observe that we usually have for conjunction:

    α → (β → γ)  ==  α ∧ β → γ

So we can write the rule as:

       Γ ⊢ α1    ....  Γ ⊢ αn
    -----------------------------
      Γ,  α1 ∧  ... ∧ αn → β ⊢ β

Now use comman and Prolog implication and you can write it:

       Γ ⊢ α1    ....  Γ ⊢ αn
    -----------------------------
      Γ, (β :- α1, .., αn) ⊢ β

Thats basically the declarative reading,
reading ⊢ as "is true":

"The goal β is true if the subgoals ​α1, .., αn are all true."

Bye

Mild Shock schrieb:

Hi,sub

There are some reduction techniques that more
or less work for natural deduction. But its
not so easy, you need Long Head Normal form

and stuff. But Prolog code, a description of it,
has been published for example here. Guess who
wrote the Prolog code paper?

August 1988
https://www.researchgate.net/publication/322069446

Its based on the original Howard paper which uses a
multi premisse rule. So its not a rule with a fixed
arity. Namely its this rule:

     Γ ⊢ α1    ....  Γ ⊢ αn
  -----------------------------
    Γ, α1 → ...  → αn → β ⊢ β

You can use the above for reduction. And it
has a Natural Deduction Flair. You can also related
the above rule to Sequent calculus.

Its quite a Christmas Miracle.

Bye

Mild Shock schrieb:

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

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)