Path: eternal-september.org!news.eternal-september.org!feeder3.eternal-september.org!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: Re: A Christmas Miracle (Was: Curry-Howard Correspondence where?)
Date: Sat, 21 Dec 2024 21:20:08 +0100
Message-ID: <vk77tr$1jg02$1@solani.org>
References: <vjks2t$sghb$1@solani.org> <vjksaq$sgo6$1@solani.org>
 <vjksdb$sgo6$2@solani.org> <vjs63g$1m603$1@dont-email.me>
 <vk76kj$1jf9l$1@solani.org> <vk772u$1jfhe$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sat, 21 Dec 2024 20:20:11 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="1687554"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.19
Cancel-Lock: sha1:cc3Eg98VK8q6RfQ+9rBZU5TFw/8=
X-User-ID: eJwNyskBAzEIA8CWAJurHEeC/kvYzHv8hAbyhsf19WV3DPi7prlce+icPLol/hY6T8CCjy3tX5uWASK9KKfkA38oFmg=
In-Reply-To: <vk772u$1jfhe$1@solani.org>

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