Re: What are Simple Types (Was: Proofs as programs)

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