Re: A Christmas Miracle (Was: Curry-Howard Correspondence where?)

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 `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> >
>

>

>