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: A Christmas Miracle (Was: Curry-Howard Correspondence where?)
Date: Sat, 21 Dec 2024 21:05:50 +0100
Message-ID: <vk772u$1jfhe$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>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sat, 21 Dec 2024 20:05:50 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="1687086"; 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:kUTPql5if/SRMP+qSIG5WSeNTIU=
In-Reply-To: <vk76kj$1jf9l$1@solani.org>
X-User-ID: eJwFwQkBwDAIA0BLUEgocnhW/xJ2B6Nywgk6Hl6lV11H+Dlfnk9JE9uNFUOVnRYJjOAxO7QJ6bCZu9RI6A8yPBRm
Bytes: 5169
Lines: 119

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