Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Julio Di Egidio <julio@diegidio.name>
Newsgroups: sci.logic
Subject: Re: What are Simple Types (Was: Proofs as programs)
Date: Thu, 19 Dec 2024 02:51:13 +0100
Organization: A noiseless patient Spider
Lines: 32
Message-ID: <vjvu6i$2epso$2@dont-email.me>
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> <vjvsu1$2epso$1@dont-email.me>
 <vjvtc9$1ffc1$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 19 Dec 2024 02:51:14 +0100 (CET)
Injection-Info: dont-email.me; posting-host="5c82a02c1e2f107e6a78dfd6f7615e23";
	logging-data="2582424"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18x76BSdcLoeuOUzmWgxWD7ieN4lK4zkdU="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:159FpKODMPH9ZOubTcRo1I6ycEY=
In-Reply-To: <vjvtc9$1ffc1$1@solani.org>
Content-Language: en-GB
Bytes: 2497

On 19/12/2024 02:37, Mild Shock wrote:
> Julio Di Egidio schrieb:
>> On 19/12/2024 00:30, Mild Shock wrote:
>>> 
>>> It cannot be a proof term of Affine Logic, since x occurs twice.
>> 
>> That is not what affine logic means.
> 
> Well it does. It is based on the combinators B and C.
> You cannot translate a lambda expression where x occurs twice
> with B and C. You would need S.
> 
> Rule 7 and 8
> https://en.wikipedia.org/wiki/Combinatory_logic#Combinators_B,_C
> 
> With B and C, you can only translate λx.(E1 E2) if x
> occurs in E1 or E2 or none, but not in both E1 and E2.
> 
> Basically the implied requirement to have an equivalence
> between the natural deduction and the hilbert style proofs,
> that every lambda express can be translated to BCI.

<< Affine logic is a *substructural logic* whose proof theory rejects 
the structural rule of contraction. It can also be characterized as 
linear logic with weakening. >>
<https://en.wikipedia.org/wiki/Affine_logic>
<https://en.wikipedia.org/wiki/Substructural_type_system>

HTH.

-Julio