Path: ...!news.mixmin.net!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:24:21 +0100
Message-ID: <vk785m$1jg0n$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>
 <vk77tr$1jg02$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:24:22 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="1687575"; 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:KZ6SJQF3H/fQkyevXUEik3CdVKw=
In-Reply-To: <vk77tr$1jg02$1@solani.org>
X-User-ID: eJwNyskBwCAMA7CZguMc44Ah+4/Q6i0iLJQeDOdwfM7UurkS1ttc8ovs/wDKiT54WmBPGKzK91OTR6jeed8HR04VTQ==
Bytes: 7520
Lines: 191

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 
========== REMAINDER OF ARTICLE TRUNCATED ==========