The Task is called the Inhabitation Problem (Was: /* A */ and /* B */ are different)

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
>