Path: ...!news.nobody.at!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: What are Simple Types (Was: Proofs as programs)
Date: Thu, 19 Dec 2024 00:42:19 +0100
Message-ID: <vjvmkq$1fcff$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>
 <vjsl6t$1dmbi$1@solani.org> <vjt8up$1m603$3@dont-email.me>
 <vjttuv$10v9c$1@solani.org> <vjtueg$10vjo$1@solani.org>
 <vju67k$1m603$4@dont-email.me> <vjulf8$1er6n$1@solani.org>
 <vjumaf$1erpp$1@solani.org> <vjuptb$1m602$1@dont-email.me>
 <vjvluk$1fc4q$1@solani.org> <vjvm3i$1fc4q$2@solani.org>
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: <vjvm3i$1fc4q$2@solani.org>
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
>>>
>>
>