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: Advent of Logic 2024: Friendly Reminder (Re: Advent of Logic
 2024: Specification and Deadline)
Date: Tue, 24 Dec 2024 00:09:57 +0100
Message-ID: <vkcqk5$19bn1$1@solani.org>
References: <vjks2t$sghb$1@solani.org> <vk2i2c$1gvoe$1@solani.org>
 <vk6kfv$15r1k$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 23 Dec 2024 23:09:57 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="1355489"; 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:6cNnyAENKY7uhB9GmWg4nLVY50s=
X-User-ID: eJwFwQkBwDAIA0BLZUCgcnga/xJ25wrBhMFhTmeyxJtfaa0xtqy18+sZhMg9tX3Jc9/BhoLVL1KLkaK04Q9/lRaz
In-Reply-To: <vk6kfv$15r1k$1@solani.org>
Bytes: 3700
Lines: 94

Ok, I made a solution for Weekend 3,
first I made minimal logic. I opted for
Lambda Expressions with de Brujin indexes:

/* 4 positive test cases */

% ?- between(1,13,N), search(typeof(X, [], ((a->a)->(a->a))), N, 0).
% N = 2,
% X = lam((a->a), 0) .

% ?- between(1,13,N), search(typeof(X, [], (a->((a->b)->b))), N, 0).
% N = 5,
% X = lam(a, lam((a->b), 0*1)) .

% ?- between(1,13,N), search(typeof(X, [], (a->(b->a))), N, 0).
% N = 3,
% X = lam(a, lam(b, 1)) .

% ?- between(1,13,N), search(typeof(X, [], ((a->(a->b))->(a->b))), N, 0).
% N = 7,
% X = lam((a->a->b), lam(a, 1*0*0)) .

For example the 2nd solution with de Brujin indexs
can be read without de Brujin indexes as follows:

λx:a.λy:(a->b).(y x)    :    (a->((a->b)->b))

https://gist.github.com/Jean-Luc-Picard-2021/db6f71f66781838c98ee8b828eb5b9c2#file-minimal-p

Mild Shock schrieb:
> Hi,
> 
> Friendly Reminder that the Deadline 24. December 2024
> is approaching. Please be aware that Weekend 3 asks for
> Natural Deduction, where (E⊃) and Modus Ponens are synonymous:
> 
> /* Scope of Weekend 3 */
> 
>    C, X  ⊢  Y
> -------------- (I⊃)
>    C ⊢ X ⊃ Y
> 
>    C ⊢ X    C ⊢ X ⊃ Y
> --------------------- (E⊃) /* Also known as Modus Ponens */
>         C ⊢ Y
> 
> 
> Simply Types and its Curry Howard is primarily defined
> for Natural Deduction. Extracting Lambda Experessions
> from Non-Natural Deduction is a little bit more complicated.
> 
> So Weekend 3 is NOT for Sequent Calculus:
> 
> /* Not Scope of Weekend 3 */
> 
>    C, X  ⊢  Y
> -------------- (R⊃)
>    C ⊢ X ⊃ Y
> 
>    C ⊢ X    C, Y ⊢ Z
> --------------------- (L⊃)
>      C, X ⊃ Y ⊢ Z
> 
> Bye
> 
> Mild Shock schrieb:
>> Specification:
>>
>>
>> Weekend 2:
>> -----------
>> - Input = Atom            % Propositional variable
>>          | Input -> Input  % Implication
>>
>> - Output = B               % B Axiom Schema
>>           | C               % C Axiom Schema
>>           | I               % I Axiom Schema
>>           | (Output Output) % Modus Ponens
>>
>> Weekend 3:
>> -----------
>> - Input = Atom            % Propositional variable
>>          | Input -> Input  % Implication
>>
>> - Output = Variable         % Repetition
>>           | λVariable.Output % Assumption & Detachment
>>           | (Output Output)  % Modus Ponens
>>
>>
>> Deadline:
>>
>> 24. December 2024
>>
>