Curry-Howard Correspondence where? (Was: Proofs as programs (Was: Advent of Logic 2024: Weekend 3))

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>