/* A */ and /* B */ are different (Was: Proofs as programs)

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