Path: ...!news.nobody.at!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: What are Simple Types (Was: Proofs as programs) Date: Thu, 19 Dec 2024 00:42:19 +0100 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Wed, 18 Dec 2024 23:42:18 -0000 (UTC) Injection-Info: solani.org; logging-data="1552879"; 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:ovutOpDcbbQPfW+4yxkqlznoR9Y= In-Reply-To: X-User-ID: eJwFwQkBwDAIA0BL/FA5aUf8S9hdemm9jsqKZNKG33rfOL27hAwehXLmftpzQ/MAEDO89lyHaQwZKuMK/HJnFeM= Bytes: 4538 Lines: 125 Hi, What I don't know yet, is how to assure that the context is used affine. Non-affine modus ponens can be seen as, where E is what is common in both contexts, and the comma is disjoint union: G, E |- A -> B E, D |- A -------------------------------- G, E, D |- B In linear logic the linear implication uses a splitting context: G |- A -o B D |- A -------------------------------- G, D |- B This is unlike intuitionistic logic, which uses the Non-affine modus ponense. But the affine modus ponens uses a splitting context. How implement proof search efficiently for splitting context? I have some idea based on DCG. But I didn't find a paper yet showing such a DCG based search for linear logic. Bye Mild Shock schrieb: > Hi, > > The typing rules for WE3 are similar to WE2. > The changes are: > > - WE2 doesn't require a context > - WE3 requires a context > - WE2 has only modus ponense and constants > - WE3 has additionally deduction theorem and variables > > See also here what WE3 requires: > > https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus#Typing_rules > > Bye > > Mild Shock schrieb: >> The requirement for week 3 is explicitly lambda expressions: >> >>> Create a proof search in Simple Types, >>> that finds Lambda Expressions as proof, >>> for a given formula in propositional logic. >>> >>> The logic is the same as in Weekend 2. >> >> >> For Affine Logic the lambda expressions should have a funny property: >> >> - A variable occurs only once unbound in the bound scope. >> >> For example this here, although it has a simple type: >> >> λ y:A λ x:A->A. x (x y) >> >> It cannot be a proof term of Affine Logic, since x occurs twice. >> >> Some testing showed you don't produce lambda expressions: >> >> You produce: >> >>> But I am not familiar with this proof display: >>> >>> [ >>>    impI((p->0)) >>>    impI((p->0)) >>>    [ >>>      impE1(1:(p->q)) >>>      impI(p) >>>      [ >>>        impE1(1:p) >>>        unif(2:p) >>>      ] >>>      [ >>>        impE2(1:0) >>>        botE(3:0) >>>      ] >>>    ] >>>    [ >>>      impE2(1:p) >>>      [ >>>        impE1(1:p) >>>        unif(2:p) >>>      ] >>>      [ >>>        impE2(1:0) >>>        unif(3:0) >>>      ] >>>    ] >>> ] >> >> Julio Di Egidio schrieb: >>> On 18/12/2024 15:30, Mild Shock wrote: >>> >>>> Maybe your work qualifies for Weekend 3. >>> >>> In fact, I have replied to the WE3 announcement. >>> >>>> I don't know yet. You have to tell us. Do >>>> you think it implements a Natural Deduction >>>> with Simple Types proof extraction? >>> >>> It implements "affine intuitionistic propositional logic", and I am >>> getting to evaluation/compilation which is the functional side (more >>> details in my initial reply): so, sure, I even classify my reduction >>> rules as intros vs elims... >>> >>> What is the deadline?  I don't know what WE is 3. >>> >>> -Julio >>> >> >