Path: ...!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 02:37:13 +0100
Message-ID: <vjvtc9$1ffc1$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> <vjvsu1$2epso$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 19 Dec 2024 01:37:13 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="1555841"; 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:eHIZxwYDJlXgxYHeNun5P4pD3K4=
In-Reply-To: <vjvsu1$2epso$1@dont-email.me>
X-User-ID: eJwFwYkBwCAIA8CVQE1sxkGe/UfoHTadeQ/Bg8EsJntVqkbKUPFF9I5YiiSeNr88Nu6A2ZXY8zhXXl/b8Ad2vxYN
Bytes: 2063
Lines: 19

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.

Bye