TEST
7
matricola: ______________________________
nome (solo se non si ricorda la matricola):
__________________________________
- The term λnmfx.nf(mfx) represents
the binary addition function. Write the term representing the
ternary addition.
- Complete, if possible, the following typing derivation,
filling the missing parts
{z:
, x: } |- z :
{z: ,
x: } |- x :
-----------------------------------------------------------------------------------
{z:
, x: } |- zx
:
{z:
, x: } |- x :
----------------------------------------------------------------------------------------------------
{z: ,
x: } |- (zx)x
:
------------------------------------------------
{z:
} |- λx.zxx
:
- What is the Substitution Lemma?