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: The Task is called the Inhabitation Problem (Was: /* A */ and /* B */
 are different)
Date: Mon, 23 Dec 2024 00:56:28 +0100
Message-ID: <vka8vc$17vca$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>
 <vk1lqu$2s7tr$1@dont-email.me> <vk9hb1$innf$2@dont-email.me>
 <vka8m6$17val$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 22 Dec 2024 23:56:28 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="1310090"; 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:evyrwYs6A5AJL0OaAoT9wNN88Gc=
X-User-ID: eJwNyMkBACAIA7CVFDlkHGxl/xH0k0ds+XSEurlaWwfAqdnELhvJo3KkeMD9SULL0L30T+kNYWTw3lySGFkPnPgXeg==
In-Reply-To: <vka8m6$17val$1@solani.org>
Bytes: 3630
Lines: 82

Hi,

The Task of Weekend 2 and Weekend 3 is called
the Inhabitation Problem. Its different from
Syntax-directed rule system.

https://en.wikipedia.org/wiki/Type_inhabitation

In the solution to Weekend 2 you see how
Types can be inhabitated by Combinatorial
Expressions. The code is here:

/* vanilla interpreter with typeof/2 counting */
% search(+Goal, +Integer, -Integer)
search(true, N, N).
search((A,B), N, M) :-
    search(A, N, H),
    search(B, H, M).
search(typeof(P, T), N, M) :- N>0, H is N-1,
    clause(typeof(P, T), B),
    search(B, H, M).
search(unify_with_occurs_check(A,B), N, N) :-
    unify_with_occurs_check(A,B).
https://gist.github.com/Jean-Luc-Picard-2021/bc829e6c002b955a51a49ae3bf384c72

It uses a form of iterative deepening,
and finds shortes Combinatorial
Expressions first.

You can apply the same search in Weekend 3,
and find Lambda Expressions instead of
Combinatorial Expressions.

But Weekend 3 should be Natural Deduction
and not Sequent Calculus. You could solve
Sequent Calculus as Weekend 4.

Mild Shock schrieb:
> 
> Its different from yours. Yours has, it is
> wrongly labled should be impL:
> 
> % (C,X->Y=>Z) --> [(C=>X),(C,Y=>Z)]    /* A */
> reduction(impE, (C0=>Z), [C=>X,[Y|C]=>Z], [H]) :-
> use_hyp((_->_), C0, (X->Y), C, H).
> 
> On the other hand Hindley–Milner has [App],
> which is the real impE:
> 
> % (C=>Y) --> [(C=>X->Y),(C=>X)]    /* B */
> https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Syntax-directed_rule_system 
> 
> 
> /* A */ and /* B */ are different:
> 
> /* A */ Belongs to Sequent Calculus
> in Gentzens Paper the Systems LJ and LK
> 
> /* B */ Belongs to Natural Deduction,
> in Gentzens Paper the Systems NJ and NK
> 
> Algorithm W is what a Prolog interpreter would
> do, when the Proof Term is given and when we
> want to find the Principal Type.
> 
> For Weekend 3 the task is different, the Type
> is given and we want to find the Proof Term.
> 
> Julio Di Egidio schrieb:
>> On 19/12/2024 18:40, Julio Di Egidio wrote:
>>
>>> My interpretation might be unorthodox, anyway here is concretely what 
>>> I am doing (a far better approximation that is): 
>>> <https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Syntax-directed_rule_system> 
>>>
>>
>> That is, Hindley-Milner upside down:
>> a *closed* universe with Prop on top...
>>
>> -Julio
>>
>