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 Newsgroups: sci.logic Subject: Re: A Christmas Miracle (Was: Curry-Howard Correspondence where?) Date: Sat, 21 Dec 2024 21:20:08 +0100 Message-ID: References: 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: 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 >>> >>> >>> >> >