"QQMJDBUJWF *OUFSTFDUJPO 5ZQFT
CZ

9VF 9V薛旭" UIFTJT TVCNJUUFE JO QBSUJBM GVMêMMNFOU PG UIF SFRVJSFNFOUT GPS
UIF EFHSFF PG .BTUFS PG 1IJMPTPQIZ
BU ѮF 6OJWFSTJUZ PG )POH ,POH

+BOVBSZ "CTUSBDU PG UIFTJT FOUJUMFEi"QQMJDBUJWF *OUFSTFDUJPO 5ZQFTw
4VCNJUUFE CZ
9VF 9VGPS UIF EFHSFF PG .BTUFS PG 1IJMPTPQIZ
BU ѮF 6OJWFSTJUZ PG )POH ,POH
JO +BOVBSZ " OFX QSPHSBNNJOH MBOHVBHF JT PѫFO FMBCPSBUFE CZ JOUSPEVDJOH EJĒFSFOU GFBUVSFT 4PNF
PG UIPTF GFBUVSFT BSF OPU PSUIPHPOBM BOE UIFJS DPNCJOBUJPO SJTLT CSFBLJOH UIF TBGFUZ PG UIFXIPMF TZTUFN FTQFDJBMMZ JO TUBUJDBMMZ UZQFE MBOHVBHFT "MTP UIF OFXMZ DPNJOH GFBUVSF JT
DPOWFOUJPOBMMZ SFBTPOFE JO JTPMBUJPO PS JO B SBUIFS NJOJNJTFE DBMDVMVT *U JT OPU TVSQSJTJOH GPS
MBOHVBHF SFTFBSDIFST BOE JNQMFNFOUFST UP EFTJSF B HFOFSBM GSBNFXPSL UIBU DPOUBJOT GFBUVSFTBT NVDI BT QPTTJCMF BOE IBT TBMJFOU FYUFOTJCJMJUZ *OUFSTFDUJPO UZQFT BSF B OJDF êU GPS UIJTQVSQPTF
$BMDVMJ XJUI JOUFSTFDUJPO UZQFT IBWF CFFO VTFE PWFS UIF ZFBST UP NPEFM WBSJPVT GFBUVSFTJODMVEJOH PWFSMPBEJOH FYUFOTJCMF SFDPSET BOE NPSF SFDFOUMZ OFTUFE DPNQPTJUJPO BOE SFUVSOUZQF PWFSMPBEJOH /FWFSUIFMFTT OP QSFWJPVT DBMDVMVT TVQQPSUT BMM UIPTF GFBUVSFT BU PODF
*O UIJT UIFTJT XF TUVEZ FYQSFTTJWF DBMDVMJ XJUI JOUFSTFDUJPO UZQFT BOE B NFSHF PQFSBUPS
0VS êSTU DBMDVMVT TVQQPSUT BO VOSFTUSJDUFE NFSHF PQFSBUPS XIJDI JT BCMF UP TVQQPSU BMM UIFGFBUVSFT BOE JT QSPWFO UP CF UZQF TPVOE )PXFWFS UIF TFNBOUJDT JT OPOEFUFSNJOJTUJD *O
UIF TFDPOE DBMDVMVT XF FNQMPZ B QSFWJPVTMZ QSPQPTFE EJTKPJOUOFTT SFTUSJDUJPO UP NBLF UIFTFNBOUJDT EFUFSNJOJTUJD 4PNF GPSNT PG PWFSMPBEJOH BSF GPSCJEEFO CVU BMM PUIFS GFBUVSFT BSF
TVQQPSUFEѮF NBJO DIBMMFOHF JO UIF EFTJHO JT SFMBUFE UP UIF TFNBOUJDT PG BQQMJDBUJPOT BOE SFDPSEQSPKFDUJPOT 8F QSPQPTF BO BQQMJDBUJWF TVCUZQJOH SFMBUJPO UIBU FOBCMFT UIF JOGFSFODF PG SFTVMUUZQFT GPS BQQMJDBUJPOT BOE QSPKFDUJPOT $PSSFTQPOEJOHMZ UIFSF JT BO BQQMJDBUJWF EJTQBUDIJOHSFMBUJPO UIBU JT VTFE GPS UIF EZOBNJD TFNBOUJDT ѮF UXP DBMDVMJ BOE UIFJS QSPPGT BSF GPSNBMJTFE JO UIF $PR UIFPSFN QSPWFS BOE XF IBWF B QSPUPUZQF JNQMFNFOUBUJPO BT XFMM"O BCTUSBDU PG  XPSET

5P NZ CFMPWFE QBSFOUT

%ĞĜĥĚīĚĭĢĨħ
* EFDMBSF UIBU UIJT UIFTJT SFQSFTFOUT NZ PXO XPSL FYDFQU XIFSF EVF BDLOPXMFEHNFOU JT NBEF
BOE UIBU JU IBT OPU CFFO QSFWJPVTMZ JODMVEFE JO B UIFTJT EJTTFSUBUJPO PS SFQPSU TVCNJUUFE UPUIJT 6OJWFSTJUZ PS UP BOZ PUIFS JOTUJUVUJPO GPS B EFHSFF EJQMPNB PS PUIFS RVBMJêDBUJPOT
9VF 9V+BOVBSZ J

"ĜĤħĨİĥĞĝĠĦĞħĭĬ
* UIBOL
r #SVOP $ E 4 0MJWFJSB UIF CFTU TVQFSWJTPS * IBWF FWFS IBEr /JOHOJOH 9JF +JOYV ;IBP 9VFKJOH )VBOH :BPEB ;IPV #BCFS 3FINBO .JOHRJ 9VF:BP[IV 4VO 8FOKJB :F $IFO $VJ +JOIBP 5BO BOE 4IFOHZJ +JBOH GPS UIFJS DPOUJOVPVT 2" TVQQPSU HFOFSPVT BEWJDF FOMJHIUFONFOU WBMVBCMF BOTXFST UP NZ OVNFSPVTEVNC RVFTUJPOT RVJDL BOE DMFWFS TVHHFTUJPOT JO NZ SFTFBSDI BOE MJGF
r "UTVTIJ *HBSBTIJ 4ÊSHJP -PVSFOÉP BOE 5T[ )PO :VFO GPS UIFJS DPNNJUUFF XPSL PG UIFTJTGFFECBDL BOE FYBNJOBUJPOr +JBORJBP -V )BP :V 5FOH ;IPOH 9JOIBP ;IBOH :V[IF ;IBOH .JOIF ;IBOH .FOHIVJ
2JO 9V 8BOH BOE 4IVOSBO ;IBOH GPS UIFJS MBTUJOH GSJFOETIJQr 5JBO -BO ;IJ -J BOE .JVNJV GPS UIFJS IPTU PG NZ êSTU ZFBS JO )POH ,POH
r .Z QBSFOUT GPS UIFJS VODPOEJUJPOBM TVQQPSUJJJ$ĨħĭĞħĭĬ
%ĞĜĥĚīĚĭĢĨħ

Ģ"ĜĤħĨİĥĞĝĠĦĞħĭĬ

ĢĢĢ-ĢĬĭ Ĩğ 'ĢĠĮīĞĬ

ĢıϚ*ħĭīĨĝĮĜĭĢĨħϚ

.PUJWBUJPO                                   





0WFSMPBEJOH                              





3FUVSO UZQF PWFSMPBEJOH                        





&YUFOTJCMF 3FDPSET                          





/FTUFE $PNQPTJUJPO                          



1SPCMFNT BOE $IBMMFOHFT                           





*OGFSFODF PG 1SPKFDUJPOT BOE "QQMJDBUJPOT              





%ZOBNJD 4FNBOUJDT                          





"NCJHVJUJFT JO UIF %FTJHO 4QBDF                   ,FZ *EFBT BOE $POUSJCVUJPO                          





"QQMJDBUJWF 4VCUZQJOH                         





5%04 GPS 0WFSMPBEJOH                        





5XP $BMDVMJ                              





'JSTUDMBTT $VSSJFE 0WFSMPBEFE 'VODUJPOT              





4VNNBSZ                                



0VUMJOF BOE 1VCMJTIFE XPSL                          








ϛ

#ĚĜĤĠīĨĮħĝ

ϚϜ



4JNQMZ 5ZQFE λ$BMDVMVT XJUI 4VCUZQJOH                   





4JNQMZ 5ZQFE λ$BMDVMVT                       





4VCUZQJOH                               





#JEJSFDUJPOBM 5ZQJOH                          





.FUBUIFPSZ                              W

$POUFOUT





Ϝ



*OUFSTFDUJPO 5ZQFT                           





.FSHF 0QFSBUPS                            





"QQMJDBUJPOT PG .FSHF 0QFSBUPS                   %VOêFMET $BMDVMVT                               





4ZOUBY                                 





4VCUZQJOH BOE 5ZQJOH                         





&MBCPSBUJPO 4FNBOUJDT                         



5ZQF%JSFDUFE 0QFSBUJPOBM 4FNBOUJDT                     


ϛϞ



5ZQFT                                      





4VCUZQJOH BOE #$% 4VCUZQJOH                        





4VCUZQJOH                               





#$% 4VCUZQJOH                            *OUFSTFDUJPO 4VCUZQJOH BOE 0WFSMPBEJOH                   





*OUFSQSFUBUJPO PG 4VCUZQJOH 3VMFT                   





*OUFSTFDUJPO 4VCUZQJOH 1BSUJBMMZ                   





$IBMMFOHFT PG "QQMJDBUJPO 5ZQJOH                       





"QQMJDBUJPO .PEF                               





"QQMJDBUJWF 4VCUZQJOH                             





3FDPSE 1SPKFDUJPO                               





.FUBUIFPSZ                                   " $ĚĥĜĮĥĮĬ İĢĭġ "ħ 6ħīĞĬĭīĢĜĭĞĝ .ĞīĠĞ 0ĩĞīĚĭĨī

ϝϚ



4ZOUBY                                      





5ZQJOH                                     





5ZQJOH PG "QQMJDBUJPO BOE 1SPKFDUJPO                 





&YBNQMFT                                





1SPQFSUJFT PG 5ZQJOH                          



4FNBOUJDT                                    





$BTUJOH                                 





"QQMJDBUJWF %JTQBUDIJOH                        





0QFSBUJPOBM 4FNBOUJDT                        

5ZQF 4PVOEOFTT                                





*TPNPSQIJD 4VCUZQJOH                         





5ZQF 4PVOEOFTT                            







WJ



"ĩĩĥĢĜĚĭĢįĞ 4ĮěĭĲĩĢħĠϝ*OUFSTFDUJPO 5ZQFT BOE .FSHF 0QFSBUPS                    

$POUFOUT
Ϟ

ϟ

Ϡ

ϡ

" $ĚĥĜĮĥĮĬ İĢĭġ " %ĢĬģĨĢħĭ .ĞīĠĞ 0ĩĞīĚĭĨī

ϝϢ



%JTKPJOUOFTT                                   





%JTKPJOUOFTT BOE "QQMJDBUJWF 4VCUZQJOH                    





5ZQJOH                                     





%ZOBNJD 4FNBOUJDT                              





5ZQF 4PVOEOFTT BOE %FUFSNJOJTN                      *ĦĩĥĞĦĞħĭĚĭĢĨħ

ϞϞ



4UBUJDT                                      





5ZQFT BOE 5FSNT                            





4VCUZQJOH                               





"QQMJDBUJWF 4VCUZJQOH                         





5ZQJOH                                 





%ZOBNJDT                                    





5PVS                                       3ĞĥĚĭĞĝ 8ĨīĤ

ϟϜ



*OUFSTFDUJPO 5ZQFT .FSHFT BOE 0WFSMPBEJOH                 





λ$BMDVMVT                                  





5ZQF $MBTTFT                                  





4FNBOUJD 4VCUZQJOH                              





.VMUJNFUIPET BOE .VMUJQMF %JTQBUDIJOH                   $ĨħĜĥĮĬĢĨħ Ěħĝ 'ĮĭĮīĞ 8ĨīĤ

ϟϢ



$PODMVTJPO                                   





'VUVSF 8PSL                                  





"QQMJDBUJPO .PEF                           





#JEJSFDUJPOBM 5ZQJOH                          





"NCJVHVJUJFT                             





#FTU.BUDI "QQSPBDI                         





%JTKPJOU 1PMZNPSQIJTN                        





$PNQJMF UP 3BDLFU                           #ĢěĥĢĨĠīĚĩġĲ

ϠϜ

WJJ

-ĢĬĭ Ĩğ 'ĢĠĮīĞĬ
/FTUFE $PNQPTJUJPO JO &YQSFTTJPO 1SPCMFN                 

45-$ 5ZQJOH                                  





45-$ 0QFSBUJPOBM 4FNBOUJDT                         





45-$ 4VCUZQJOH                                





#JEJSFDUJPOBM 5ZQJOH                              





%VOêFMET 4VCUZQJOH                              





%VOêFMET 5ZQJOH                                





4VCUZQJOH                                    





4QMJUUBCMF 5ZQFT BOE #$% 4VCUZQJOH                     





"QQMJDBUJWF 4VCUZQJOH 4UBDL                        





"QQMJDBUJWF 5ZQJOH                               





"QQMJDBUJWF 4VCUZQJOH                             





&YBNQMFT PG "QQMJDBUJWF 4VCUZQJOH XJUI EJĒFSFOU DPNQPTJUJPO PQFSBUPST  





#JEJSFDUJPOBM 5ZQJOH                             





$BTUJOH                                     





"QQMJDBUJWF %JTQBUDIJOH                            





0QFSBUJPOBM 4FNBOUJDT                             





*TPNPSQIJD 4VCUZQJOH                             





5PQMJLF UZQFT                                  





"MHPSJUINJD %JTKPJOUOFTT                           





#JEJSFDUJPOBM 5ZQJOH %JTKPJOUOFTT                      





$BTUJOH %JTKPJOUOFTT





"QQMJDBUJWF %JTQBUDIJOH %JTKPJOUOFTT                   





0QFSBUJPOBM 4FNBOUJDT %JTKPJOUOFTT                                                 JYϚ *ħĭīĨĝĮĜĭĢĨħ
ϚϚ .ĨĭĢįĚĭĢĨħ
*OWFOUJOH OFX QSPHSBNNJOH MBOHVBHFT JT OP MPOHFS CJH OFXT JO SFDFOU ZFBST 'PS OFX QSPHSBNNJOH MBOHVBHFT B QBSBEJHN PS QSJODJQMF JT VTVBMMZ FTUBCMJTIFE êSTU XIJDI XJMM CF FMBCPSBUFE CZ JOUSPEVDJOH EJĒFSFOU GFBUVSFT 4PNF PG UIPTF GFBUVSFT BSF OPU PSUIPHPOBM BOEUIFJS DPNCJOBUJPO SJTLT CSFBLJOH UIF TBGFUZ PG UIF XIPMF TZTUFN FTQFDJBMMZ JO TUBUJDBMMZ UZQFEMBOHVBHFT 0O UIF PUIFS IBOE QSPHSBNNJOH MBOHVBHFT BSF OPU EFTJHOFE BU PODF *O SFBMJUZ NBOZ GFBUVSFT BSF FYUFOEFE BѫFS B QSPUPUZQF JT TFUUMFE ѮVT FYUFOTJCJMJUZ JT UIF QSJNBSZDPODFSO XIFO EFTJHOJOH QSPHSBNNJOH MBOHVBHFT*O B UIFPSFUJDBM TFUUJOH UIF OFXMZ DPNJOH GFBUVSF JT DPOWFOUJPOBMMZ SFBTPOFE JO JTPMBUJPOPS JO B SBUIFS NJOJNJTFE DBMDVMVT ѮF DPNCJOBUJPO PG UIF OFX GFBUVSFT BOE PUIFS FYJTUJOHGFBUVSFT XJMM OPU CF FYBNJOFE UIPSPVHIMZ NBLJOH NPSF DPNQMFUF MBOHVBHFT IBSE UP NPEFMNBJOUBJO BOE FYUFOE *U JT OPU TVSQSJTJOH GPS MBOHVBHF SFTFBSDIFST BOE JNQMFNFOUFST UP EFTJSF
B HFOFSBM GSBNFXPSL UIBU DPOUBJOT GFBUVSFT BT NVDI BT QPTTJCMF BOE IBT TBMJFOU FYUFOTJCJMJUZ*OUFSTFDUJPO UZQFT BSF B OJDF êU UP TFSWF BT B HFOFSBM GSBNFXPSL UP NPEFM NBOZ GFBUVSFT
BSHVFE JO %VOêFME <>iPVS HPBM JT UP VTF JOUFSTFDUJPOT BOE VOJPOT BT HFOFSBM NFDIBOJTNT GPS FODPEJOHMBOHVBHF GFBUVSFT TP XF SFBMMZ TIPVME EP JU JO GVMM HFOFSBMJUZ PS OPU BU BMMu*OUFSTFDUJPO UZQFT <#BSFOESFHU FU BM  $PQQP FU BM  1PUUJOHFS  3FZOPMET
> IBWF B MPOH IJTUPSZ JO QSPHSBNNJOH MBOHVBHFT ѮFZ XFSF PSJHJOBMMZ JOUSPEVDFE UP BT
TJHO NFBOJOH UP DBOPOJDBM GPSNT JO TUSPOHMZ OPSNBMJTJOH MBNCEB UFSNT CZ 1PUUJOHFS <>
3FZOPMET <> XBT UIF êSTU UP QSPNPUF UIF VTF PG JOUFSTFDUJPO UZQFT JO QSBDUJDBM QSPHSBNNJOH )F JOUSPEVDFE B NFSHF PQFSBUPS UIBU FOBCMFT CVJMEJOH WBMVFT XJUI NVMUJQMF UZQFTXIFSF UIF NVMUJQMF UZQFT BSF NPEFMMFE BT JOUFSTFDUJPO UZQFT %VOêFME <> SFêOFE UIFNFSHF PQFSBUPS UP BEE TJHOJêDBOU BEEJUJPOBM FYQSFTTJWF QPXFS PWFS UIF PSJHJOBM GPSNVMBUJPOCZ 3FZOPMET 0WFS UIF ZFBST UIFSF IBWF CFFO TFWFSBM DBMDVMJ XJUI JOUFSTFDUJPO UZQFT FRVJQQFEXJUI B NFSHF PQFSBUPS BOE FOBCMJOH EJĒFSFOU GFBUVSFT PWFSMPBEFE GVODUJPOT <$BTUBHOB FU BM
 %VOêFME > SFUVSO UZQF PWFSMPBEJOH <.BSOUJSPTJBO FU BM > FYUFOTJCMF SFDPSET <%VOêFME  3FZOPMET > BOE OFTUFE DPNQPTJUJPO <#J FU BM  )VBOH FU BM >

 *OUSPEVDUJPO*O UIF GPMMPXJOH QBSU PG UIJT DIBQUFS XF HJWF BO PWFSWJFX PG UIFTF GFBUVSFT FODPEFE CZJOUFSTFDUJPO UZQFT BOE TIPX UIFJS JOUFSBDUJPOTϚϚϚ 0įĞīĥĨĚĝĢħĠ
'VODUJPO PWFSMPBEJOH JT B GPSN PG QPMZNPSQIJTN XIFSF UIF JNQMFNFOUBUJPO PG GVODUJPOTDBO WBSZ EFQFOEJOH PO UIF EJĒFSFOU UZQFT PG BSHVNFOUT UIBU BSF BQQMJFE CZ GVODUJPOT ѮFSF
BSF NBOZ XBZT UP SFQSFTFOU UZQFT PG PWFSMPBEFE GVODUJPOT 'PS FYBNQMF TVQQPTF b?Qr JT BO
PWFSMPBEFE GVODUJPO UIBU DBO CF BQQMJFE UP FJUIFS JOUFHFST PS CPPMFBOT)BTLFMM VUJMJTFT UZQF DMBTTFT <8BEMFS BOE #MPUU > UP BTTJHO UIF UZQF a?Qr  ⇒  →ai`BM; UP b?Qr XJUI JOTUBODFT EFêOFE ѮF LFZ JEFB PG UZQF DMBTTFT JT UP DPNCJOF UIF GFBUVSF
PG QBSBNFUSJD QPMZNPSQIJTN BOE BEIPD QPMZNPSQIJTN CZ TQFDJGZJOH DPOTUSBJOUT PO UIFQPMZNPSQIJD WBSJBCMFT 1SBDUJDBMMZ JO $PWFSMPBEFE GVODUJPOT BSF SFQSFTFOUFE BT B TFU PG

DBOEJEBUF GVODUJPOT ѮF BSHVNFOUT MJTU BOE DBOEJEBUF GVODUJPOT XJMM CF VTFE JO PWFSMPBEJOH
SFTPMVUJPO CBTFE PO B MBSHF HSPVQ PG TPQIJTUJDBUFE SVMFT8JUI JOUFSTFDUJPO UZQFT XF DBO SFQSFTFOU UIF PWFSMPBEFE b?Qr GVODUJPO JO B SFMBUJWFMZ NPSF
TUSBJHIUGPSXBSE XBZ 'PS JOTUBODF UIF b?Qr GVODUJPO IBT UIF CFMPX UZQF
b?Qr : (AMi → ai`BM;)  ("QQH → ai`BM;)(FOFSBMMZ TQFBLJOH UIF UZQF PG PWFSMPBEFE GVODUJPOT JT UIF UZQF JOUFSTFDUJPO PG UIFJS EJĒFSFOU
CSBODIFT ѮF GVODUJPO b?Qr IBT UXP CSBODIFT b?QrAMi BOE b?Qr"QQH UIVT UIF UZQF PG UIFJSPWFSMPBET JT AMi → ai`BM; JOUFSTFDUFE XJUI "QQH → ai`BM;ϚϚϛ 3ĞĭĮīħ ĭĲĩĞ ĨįĞīĥĨĚĝĢħĠ
3FUVSO UZQF PWFSMPBEJOH JT BOPUIFS GPSN PG PWFSMPBEJOH ѮF DPNNPO FYBNQMF JT )BTLFMMT`2/ ,, _2/  ⇒ ai`BM; →  JU BDDFQUT B TUSJOH BOE SFUVSOT JUT QBSTFE WBMVF JOUFHFST

CPPMFBOT FUD  ѮFJS JNQMFNFOUBUJPO JT OPU EFUFSNJOFE JO GVODUJPO BQQMJDBUJPO *OTUFBE JU
JT EFUFSNJOFE CZ UIF TVSSPVOEJOH UZQF DPOUFYUT 'PS FYBNQMF bm++ U`2/ ]R]V SFUVSOT UIFJOUFHFS k JG bm++ JT UIF TVDDFTTPS GVODUJPO UIBU UBLFT BO JOUFHFS BOE SFUVSO JUT TVDDFTTPS ѮF
UZQF EFêOJUJPO XPSLT UIF TBNF XJUI b?Qr`2/ : (ai`BM; → AMi)  (ai`BM; → "QQH) .PUJWBUJPOϚϚϜ &ıĭĞħĬĢěĥĞ 3ĞĜĨīĝĬ
3FDPSET BSF VTFGVM GPS NPEFMMJOH GFBUVSFT JO 0CKFDU0SJFOUFE 1SPHSBNNJOH *O SFDPSE DBMDVMJ UIF SFDPSET BSF JOUFSQSFUFE BT PCKFDUT MBCFMT BSF NFNCFS OBNFT BTTPDJBUFE WBMVFT BSF
BUUSJCVUFT BOE NFUIPET *OIFSJUBODF DBO CF NPEFMMFE BT DPODBUFOBUJPO PG SFDPSET <$BSEFMMJ
BOE .JUDIFMM >
*O DBMDVMJ XJUI JOUFSTFDUJPO UZQFT NVMUJêFME SFDPSET DBO CF WJFXFE BT TZOUBDUJD TVHBS
{x : A, y : B} /2bm;`b iQ {x : A}  {y : B}
8JUI UIJT FODPEJOH XF PCUBJO UIF XJEUI TVCUZQJOH PG SFDPSET {li : Ti }i=1..n..n+k <: {li :Ti }1..n GPS GSFF TJODF JU JT TVCTVNFE CZ UIF TVCUZQJOH PG JOUFSTFDUJPO UZQFT A  B <: A 'PS UIF EFQUI TVCUZQJOH JU JT BMTP FBTZ UP FYUFOE UIJT SVMF JOUP UIF TVCUZQJOH PG JOUFSTFDUJPOUZQFT XJUIPVU BĒFDUJOH PUIFS SVMFT ѮF QFSNVUBUJPO SVMF JT TVCTVNFE CZ UIF DPNNVUBUJWJUZPG JOUFSTFDUJPO UZQFTϚϚϝ /ĞĬĭĞĝ $ĨĦĩĨĬĢĭĢĨħ
/FTUFE DPNQPTJUJPO SFëFDUT UIF EJTUSJCVUJWJUZ QSPQFSUJFT PG JOUFSTFDUJPO UZQFT BU UIF UFSN
MFWFM 8IFO FMJNJOBUJOH UFSNT DSFBUFE CZ UIF NFSHF PQFSBUPS VTVBMMZ GVODUJPOT BOE SFDPSETUIF SFTVMUT FYUSBDUFE GSPN OFTUFE UFSNT XJMM CF DPNQPTFE /FTUFE DPNQPTJUJPO JT OPU BO JOEFQFOEFOU GFBUVSF JU DPNFT JOUP VTF XIFO XF DPNCJOF JU XJUI BOPUIFS GFBUVSF PG JOUFSTFDUJPOUZQFT FH PWFSMPBEJOH BOE FYUFOTJCMF SFDPSET *O UIF DPOUFYU PG SFDPSET UIF EJTUSJCVUJWF TVCUZQJOH SVMF FOBCMJOH OFTUFE DPNQPTJUJPO JT{l : A}  {l : B} <: {l : A  B}
/FTUFE SFDPSE DPNQPTJUJPO JT B LFZ GFBUVSF JO $PNQPTJUJPOBM 1SPHSBNNJOH $1 <;IBOH
FU BM > *U QMBZT BO JNQPSUBOU SPMF JO TPMWJOH DIBMMFOHJOH NPEVMBSJUZ QSPCMFNT TVDI BT
UIF &YQSFTTJPO 1SPCMFN <8BEMFS > BOE NPEFMT GPSNT PG GBNJMZ QPMZNPSQIJTN <&SOTU
> 8F TIPX $1 DPEF IFSF UP JMMVTUSBUF IPX UIF $PNQPTJUJPOBM 1SPHSBNNJOH TUZMF TPMWFTUIF FYQSFTTJPO QSPCMFN JO UXP EJNFOTJPOT
1īĞĝĞğĢħĞĝ -ĚħĠĮĚĠĞ 8F TUBSU XJUI EFêOJOH UIF UZQF 1pH BOE UIF DPNQPTJUJPOBM JO
UFSGBDF //aB; 1pH EFêOFT B NFUIPE 2pH XIJDI SFUVSOT BO JOUFHFS BT UIF PVUQVU //aB;
XPSLT TJNJMBSMZ UP BO JOUFSGBDF JO +BWB BOE EFDMBSFT UXP DPOTUSVDUPST GBi BOE // 1tT XPSLTMJLF B UZQF QBSBNFUFS BOE DBO CF JOTUBOUJBUFE CZ B UZQF 'PS FYBNQMF JO UIF USBJU 2pH//1tT JT JOTUBOUJBUFE CZ 1pH 8F UIFO CVJME B DPODSFUF FYQSFTTJPO 2tT// *OUSPEVDUJPO
ivT2 1pH 4 & 2pH , AMi 'civT2 //aB;I1tT= 4 &GBi, AMi → 1tTc
//, 1tT → 1tT → 1tTc'c2pH// 4 i`Bi BKTH2K2Mib //aB;I1pH= ⇒ &UGBi
MVX2pH 4 Mc
U// 2R 2kVX2pH 4 2RX2pH Y 2kX2pHc'c2tT// 1tT 4 i`Bi (b2H7 , //aB;I1tT=) ⇒ &2tT 4 // UGBi 9V UGBi 3Vc'c"ĝĝĢħĠ 0ĩĞīĚĭĢĨħĬ "EEJOH OFX PQFSBUJPOT JT TUSBJHIUGPSXBSE XF EFêOF B OFX UZQF
S`BMi BOE DPOTUSVDU B USBJU T`BMi// CZ JOTUBOUJBUJOH 1tT CZ UZQF S`BMi JO //aB;
ivT2 S`BMi 4 & T`BMi , ai`BM; 'c
T`BMi// 4 i`Bi BKTH2K2Mib //aB;IS`BMi= ⇒ &UGBiMVXT`BMi 4 iQai`BM; Mc
U// 2R 2kVXT`BMi 4 ]U] YY 2RXT`BMi YY ] Y ] YY 2kXT`BMi YY ]V]c'c"ĝĝĢħĠ %ĚĭĚĭĲĩĞĬ 5P BEE B OFX EBUBUZQF XF FYUFOE UIF DPNQPTJUJPOBM JOUFSGBDF //aB;
XJUI B OFX DPOTUSVDUPS JmH 8F DBO UIFO JNQMFNFOU UIF USBJU 2pHJmH BOE T`BMiJmH CZ
JOTUBOUJBUJOH UIF UZQF QBSBNFUFS XJUI 1pH BOE S`BMi 8F UIFO CVJME B DPODSFUF FYQSFTTJPO
2tTJmH
ivT2 JmHaB;I1tT= 4 //aB;I1tT=  &JmH , 1tT → 1tT → 1tTc
'c2pHJmH 4 i`Bi BKTH2K2Mib JmHaB;I1pH= BM?2`Bib 2pH// ⇒ &UJmH 2R 2kVX2pH 4 2RX2pH
2kX2pHc'c
T`BMiJmH 4 i`Bi BKTH2K2Mib JmHaB;IS`BMi= BM?2`Bib T`BMi// ⇒ &UJmH 2R 2kVXT`BMi 4 ]U] YY 2RXT`BMi YY ]] YY 2kXT`BMi YY ]V]c'c2tTJmH 1tT 4 i`Bi (b2H7 , JmHaB;I1tT=) BM?2`Bib 2tT// !1tT ⇒ &Qp2``B/2 2tT 4 JmH bmT2`X2tT UGBi 9Vc'c 1SPCMFNT BOE $IBMMFOHFT'JHVSF  /FTUFE $PNQPTJUJPO JO &YQSFTTJPO 1SPCMFN/ĞĬĭĞĝ $ĨĦĩĨĬĢĭĢĨħ 5P CVJME B OFX FYQSFTTJPO XIJDI TVQQPSUT B OFX PQFSBUJPO BOE B
OFX EBUBUZQF XF VTF UIF NFSHF PQFSBUPS UP DPNQPTF UIFN UPHFUIFS 8F EFNPOTUSBUF UIJTJEFB JO 'JHVSF  8F DBO TFF UIBU UIPTF UISFF êHVSFT BSF DPNQPTFE OFTUFEMZ XJUI BMM UIFIJFSBSDIJFT DPNCJOFE UPHFUIFS
2 4 M2r 2pHJmH - T`BMiJmH - 2tTJmH !U1pH  S`BMiVc/FTUFE DPNQPTJUJPO DBO BMTP PDDVS XJUI GVODUJPOBM JOUFSTFDUJPOT VTJOH UIF CFMPX TVCUZQJOH SVMF BOE FOBCMFT UIF PWFSMPBEFE GVODUJPO UP CF DVSSJFE(A → B)  (A → C) <: A → (B  C)Ϛϛ 1īĨěĥĞĦĬ Ěħĝ $ġĚĥĥĞħĠĞĬ
8F MJTUFE TPNF GFBUVSFT UIBU JOUFSTFDUJPO UZQFT FRVJQQFE XJUI B NFSHF PQFSBUPS DBO NPEFM
/FWFSUIFMFTT OP QSFWJPVT DBMDVMVT TVQQPSUT BMM GPVS GFBUVSFT UPHFUIFS 4PNF DBMDVMJ FOBCMF
GVODUJPO PWFSMPBEJOH <$BTUBHOB FU BM > CVU QSFDMVEF SFUVSO UZQF PWFSMPBEJOH BOE OFTUFEDPNQPTJUJPO 0O UIF PUIFS IBOE DBMDVMJ XJUI EJTKPJOU JOUFSTFDUJPO UZQFT <#J FU BM 
)VBOH FU BM > TVQQPSU SFUVSO UZQF PWFSMPBEJOH BOE OFTUFE DPNQPTJUJPO CVU EJTBMMPXDPOWFOUJPOBM GVODUJPOBM PWFSMPBEJOH %VOêFMET DBMDVMVT <%VOêFME > TVQQPSUT UIF êSTUUISFF GFBUVSFT CVU OPU OFTUFE DPNQPTJUJPO ѮPTF GFBUVSFT BSF OPU DPNQMFUFMZ PSUIPHPOBM
BOE UIF JOUFSBDUJPOT CFUXFFO UIFN BSF JOUFSFTUJOH BMMPXJOH GPS OFX BQQMJDBUJPOT )PXFWFSUIF JOUFSBDUJPOT BMTP QPTF OFX UFDIOJDBM DIBMMFOHFTϚϛϚ *ħğĞīĞħĜĞ Ĩğ 1īĨģĞĜĭĢĨħĬ Ěħĝ "ĩĩĥĢĜĚĭĢĨħĬ*O USBEJUJPOBM UZQF TZTUFNT JO BQQMJDBUJPOT e1 e2 PS QSPKFDUJPOT e.l e1 JT FYQFDUFE UP IBWF BO
BSSPX UZQF BOE e JT FYQFDUFE UP IBWF B SFDPSE UZQF 4VDI DPOWFOUJPO IPXFWFS DBOOPU BQQMZ
UP PVS TZTUFN CFDBVTF DFSUBJO GPSNT PG JOUFSTFDUJPO UZQFT DBO BMTP QMBZ UIF SPMF PG BSSPX PS
SFDPSE UZQFT *O QBSUJDVMBS TVDI VTF DBTFT PG JOUFSTFDUJPO UZQFT BSF IFMQGVM GPS NPEFMMJOH *OUSPEVDUJPOPWFSMPBEFE GVODUJPOT BOE NVMUJêFME SFDPSET 'PS FYBNQMF XF LOPX UIBU b?QrAMi JT POF
CSBODI PG b?Qr XJUI UIF TVCUZQJOH TUBUFNFOU
(AMi → ai`BM;)  ("QQH → ai`BM;) <: AMi → ai`BM;'SPN UIJT FYBNQMF XF DBO TFF UIBU UIF EZOBNJD TFNBOUJDT NVTU TPNFIPX CF UZQFEFQFOEFOU
*O PVS XPSL XF GPMMPX UIF UZQFEJSFDUFE PQFSBUJPOBM TFNBOUJDT 5%04 <)VBOH FU BM >BQQSPBDI XIJDI DIPPTFT CFUXFFO NFSHFE GVODUJPOT BDDPSEJOH UP UZQF JOGPSNBUJPO EVSJOHSVOUJNF )PXFWFS FYJTUJOH 5%04 BQQSPBDIFT EP OPU TVQQPSU PWFSMPBEJOH GPS UXP SFBTPOT'JSTUMZ 5%04 SFRVJSFT NFSHFE GVODUJPOT UP CF EJTKPJOU XJUI FBDI PUIFS CVU JO UIJT DBTF UIFNFSHFE GVODUJPOT BSF OPU EJTKPJOU JF AMi → ai`BM; JT OPU EJTKPJOU XJUI "QQH → ai`BM;

CFDBVTF PG UIF DPNNPO SFUVSO UZQF ai`BM;  4FDPOEMZ FWFO JG XF XPVME TJNQMZ JHOPSF UIFEJTKPJOUOFTT SFTUSJDUJPO XF XPVME TUJMM OFFE UP QVU BO FYQMJDJU UZQF BOOPUBUJPO AMi → ai`BM;

BOE XSJUF UIF QSPHSBN BT Ub?Qr , AMi → ai`BM;V R UP TFMFDU UIF DPSSFDU JNQMFNFOUBUJPOUP BQQMZ GSPN UIF PWFSMPBEFE b?Qr GVODUJPO ѮJT JT CFDBVTF QSFWJPVT 5%04 DBMDVMJ IBWF
SFTUSJDUFE BQQMJDBUJPO SVMFT UIBU DBOOPU BDDPNNPEBUF USBEJUJPOBM PWFSMPBEJOH $MFBSMZ JO BTFUUJOH XJUI PWFSMPBEJOH IBWJOH UP XSJUF TVDI FYQMJDJU BOOPUBUJPOT XPVME CF VOTBUJTGZJOHѮFSFGPSF XF XJTI UP IBWF BO BQQSPBDI XIFSF XF DBO XSJUF PWFSMPBEFE GVODUJPOT OBUVSBMMZ" TJNJMBS QSPCMFN PDDVST VTJOH SFDPSE QSPKFDUJPOT JO FYJTUJOH 5%04 DBMDVMJ 'PS JOTUBODFUIF UZQF TZTUFN PG λi+ <)VBOH FU BM > SFRVJSFT FYQMJDJU BOOPUBUJPOT GPS QSPKFDUJPOT PG
NVMUJêFME SFDPSET XJUI EJTUJODU MBCFMT TVDI BT U&t 4 R'--&v 4 i`m2' , &t , AMi'VXt
ѮJT JT PG DPVSTF RVJUF VOOBUVSBM UP XSJUF "MUIPVHI TPVSDF MBOHVBHFT UBSHFUUJOH UIF 5%04
DBMDVMJ DBO FMJNJOBUF UIF FYQMJDJU VTF PG TVDI BOOPUBUJPOT BU UIF TPVSDF MFWFM JU XPVME CF CFUUFSUP BEESFTT UIJT QSPCMFN EJSFDUMZ JO UIF 5%04Ϛϛϛ %ĲħĚĦĢĜ 4ĞĦĚħĭĢĜĬ(JWJOH B EJSFDU TFNBOUJDT UP PWFSMPBEFE BQQMJDBUJPOT JT B OPOUSJWJBM QSPCMFN ѮBOLT UP
UIF NFSHF PQFSBUPS BOE UIF DBMMCZWBMVF TUSBUFHZ PVS PWFSMPBEFE GVODUJPOT BSF FYQFDUFEUP CF JO UIF GPSN PG OFTUFE NFSHFT BDDPSEJOH UP UIF TUSVDUVSF PG UZQFT 4P XF DBO SFBTPOBCPVU UIF EZOBNJD TFNBOUJDT BT XF EFBM XJUI UIF UZQFT 6OGPSUVOBUFMZ UIF EJTUSJCVUJWJUZ
PG TVCUZQJOH DPNQMJDBUFT UIF TUPSZ ѮF DIBMMFOHF DPNFT GSPN UIF GBDU UIBU JO PVS TFUUJOHPWFSMPBEFE GVODUJPOT BSF êSTUDMBTT ѮBU JT UIFZ DBO CF UBLFO BT BSHVNFOUT PS SFUVSOFE BT
SFTVMUT 'PS JOTUBODF XF DBO IBWF
Tb?Qr , lMBi → UAMi → ai`BM;V  U"QQH → ai`BM;V
Tb?Qr 4 λtX b?Qr 1SPCMFNT BOE $IBMMFOHFT*O UIJT TJUVBUJPO BO PWFSMPBEFE GVODUJPO JT XSBQQFE XJUI B MBNCEB BCTUSBDUJPO XIJMF JU
TIPVME BMTP CF WJFXFE BT BO PWFSMPBEFE GVODUJPO 'PS FYBNQMF XF FYQFDU UIF GPMMPXJOH UPIPME
Tb?Qr mMBi R "→ ]R]

Tb?Qr mMBi i`m2 "→ ]i`m2]*O UIF MBTU UXP DBTFT XJUI B USBEJUJPOBM BQQSPBDI UP BQQMJDBUJPOT Tb?Qr JT FYQFDUFE UP IBWFUZQF lMBi → AMi → ai`BM; BOE lMBi → "QQH → ai`BM; SFTQFDUJWFMZ 'SPN UIF QFSTQFDUJWF PG JOUFSTFDUJPO PWFSMPBEJOH Tb?Qr TIPVME CF PG UZQF UlMBi → AMi → ai`BM;V UlMBi → "QQH → ai`BM;V XIJDI IPXFWFS JT EJĒFSFOU GSPN UIF HJWFO UZQF BOOPUBUJPOѮJT BMUFSOBUJWF WJFX PG UZQFT BOE GVODUJPOT QPTFT DIBMMFOHFT UP UIF EFTJHO PG UIF TUBUJD BT XFMMBT UIF EZOBNJD TFNBOUJDTϚϛϜ "ĦěĢĠĮĢĭĢĞĬ Ģħ ĭġĞ %ĞĬĢĠħ 4ĩĚĜĞ
" QBSUJDVMBS DIBMMFOHF XJUI PWFSMPBEJOH BOE NFSHFT JT BNCJHVJUJFT "NCJHVJUJFT DBO IBQQFO
CPUI XJUI SFDPSE QSPKFDUJPOT BOEPS PWFSMPBEJOH 3FQFBUFE MBCFMT BSF BMXBZT B DPODFSO JO
EFTJHOJOH UIF DPODBUFOBUJPO PG SFDPSET 8IFUIFS UP BMMPX SFQFBUFE MBCFMT MFBET UP EJĒFSFOU
EFTJHOT PG SFDPSET "NCJHVJUJFT JO GVODUJPO PWFSMPBEJOH BSF NPSF DPNQMJDBUFE 8F JEFOUJGZUXP LFZ QSPCMFNT PG PWFSMPBEJOH BNCJHVJUJFT CFMPX"ĦěĢĠĮĢĭĢĞĬ Ĩħ ĭġĞ ĢħĩĮĭ ĭĲĩĞĬ *O MBOHVBHFT MJLF $BOE +BWB PWFSMPBEJOH DBOOPU CF

EFêOFE PO SFUVSO UZQFT BOE BNCJHVJUJFT BSF EFUFDUFE XIFO UIF JOQVU UZQFT PG PWFSMPBEFEGVODUJPOT PWFSMBQ ѮJT JT BMTP B SFBTPO XIZ NBOZ XPSLT NPEFM UIF JOQVUT PG PWFSMPBEFEGVODUJPOT BT QSPEVDU UZQFT <$BTUBHOB FU BM  %VOêFME  ,BFT > ѮF BEWBOUBHFT
BSF PCWJPVT JU JT FBTJFS UP SFTPMWF UIF DPSSFDU CSBODI CZ POMZ DPNQBSJOH UIF QSPEVDU UZQFTBOE UZQFT PG BSHVNFOUT ѮF ESBXCBDL PG UIJT NPEFM JT UIBU QSPEVDU UZQFT XJMM QSFWFOU PWFSMPBEFE GVODUJPOT UP CF DVSSJFE ѮJT JT CFDBVTF PWFSMPBEFE GVODUJPOT CBTFE PO QSPEVDU UZQFT
FYQFDU B UVQMF DPOUBJOJOH BMM UIF BSHVNFOUT BOE SFKFDU QBSUJBM BQQMJDBUJPOT ѮF DIBMMFOHF
PG NPEFMMJOH PWFSMPBEFE DVSSJFE GVODUJPOT JT UIBU QBSUJBM BQQMJDBUJPOT NBZ CF JOTVēDJFOU UP
GVMMZ EFUFSNJOF UIF JNQMFNFOUBUJPO UP UBLF GSPN UIF PWFSMPBEFE GVODUJPO ѮFTF QBJOT DBO
CF BMMFWJBUFE VTJOH JOUFSTFDUJPO UZQFT UIF NFSHF PQFSBUPS BOE UIF GFBUVSF PG OFTUFE DPNQPTJUJPOf : AMi → AMi → AMi

g : AMi → "QQH → "QQH

'PS FYBNQMF XJUI 7--; XF DBO TJNQMZ SFBTPO UIBU UIF SFTVMU PG U7--;V R i`m2 JT ; R i`m2
ѮF QSPCMFN PDDVST JO UIF QBSUJBMMZ BQQMJFE UFSN U7--;V R GPS XIJDI UIFSF BSF UXP QPTTJCMF
EFTJHO DIPJDFT ѮF êSTU DIPJDF JT UP SFKFDU UIJT BQQMJDBUJPO UFSN TJODF XF DBOOPU TFMFDU CFUXFFO PWFSMPBET UIVT GPSCJEEJOH NBOZ VTF DBTFT MJLF UIJT "OPUIFS DIPJDF JT UP BQQMZ 7 BOE *OUSPEVDUJPO; JO QBSBMMFM UP R SFTVMUJOH JO U7 RV--U; RV XIJDI IBT UIF UZQF UAMi → AMiV  U"QQH →"QQHV

"ĦěĢĠĮĢĭĢĞĬ Ĩħ ĭġĞ ĨĮĭĩĮĭ ĭĲĩĞĬ 0VUQVU UZQFT BSF VTVBMMZ OPU DPOTJEFSFE JO DPNNPOMBOHVBHFT FTQFDJBMMZ XIFO JOQVU UZQFT BSF OPU MJLFMZ UP DBVTF BNCJHVJUJFT 6OGPSUVOBUFMZ JO
B GPSNBM TZTUFN XJUI BO VOSFTUSJDUFE NFSHF PQFSBUPS XF DBO BMXBZT DSFBUF B UFSN êUUJOH CPUICSBODIFT 'PS FYBNQMF XF DBO BQQMZ b?Qr UP R--i`m2 BOE UIF SFTVMU JT ]R]--]i`m2] XIJDIQPUFOUJBMMZ MPTFT EFUFSNJOJTN TJODF UFSN ]R]--]i`m2] DBO CF SFEVDFE UP ]R] PS ]i`m2]
VOEFS UIF DBTU PG ai`BM; *O DPODMVTJPO XIBUFWFS UIF JOQVU UZQFT BSF UIFSF JT BMXBZT B SJTLUP CSFBL EFUFSNJOJTN JG UIF PVUQVU UZQFT BSF UIF TBNF VOEFS UIF DPOUFYU PG BO VOSFTUSJDUFE
NFSHF PQFSBUPS ѮFSF JT BMTP B DPODFSO JO NPEFMMJOH SFUVSO UZQF PWFSMPBEJOH TJODF UIFSF
FYJTU BNCJHVJUJFT XIFO UIF TVSSPVOEJOH DPOUFYU DBOOPU EJTUJOHVJTI CFUXFFO JOTUBODFTϚϜ ,ĞĲ *ĝĞĚĬ Ěħĝ $ĨħĭīĢěĮĭĢĨħ
ѮJT UIFTJT TUVEJFT FYQSFTTJWF DBMDVMJ XJUI JOUFSTFDUJPO UZQFT BOE B NFSHF PQFSBUPS 0VS HPBMJT UP EFTJHO DBMDVMJ UIBU EFBM XJUI BMM GPVS GFBUVSFT BU PODF BOE TUVEZ UIF JOUFSBDUJPO CFUXFFOUIFTF GFBUVSFT 0VS UXP NBJO GPDVTFT BSF PO UZQF JOGFSFODF GPS BQQMJDBUJPOT BOE SFDPSE QSPKFDUJPO BOE UIF EFTJHO PG UIF PQFSBUJPOBM TFNBOUJDT GPS TVDI DBMDVMJ 5P FOBCMF BMM UIF GFBUVSFTXF JOUSPEVDF B TQFDJBMJTFE GPSN PG TVCUZQJOH DBMMFE BQQMJDBUJWF TVCUZQJOH UP EFBM XJUI UIFëFYJCMF GPSNT PG BQQMJDBUJPOT BOE SFDPSE QSPKFDUJPO BMMPXFE CZ UIF DBMDVMJ $PSSFTQPOEJOHMZUIFSF JT BO BQQMJDBUJWF EJTQBUDIJOH SFMBUJPO UIBU JT VTFE GPS UIF EZOBNJD TFNBOUJDT *O BEEJUJPO XF FYQMPSF UIF JOUFSBDUJPOT CFUXFFO GFBUVSFT *O QBSUJDVMBS PWFSMPBEJOH BOE OFTUFEDPNQPTJUJPO FOBCMF DVSSJFE PWFSMPBEFE GVODUJPOT XIJMF NPTU QSFWJPVT XPSL <#PCSPX FU BM
 $BTUBHOB FU BM  %VOêFME  ,BFT > POMZ DPOTJEFST VODVSSJFE PWFSMPBEFEGVODUJPOTϚϜϚ "ĩĩĥĢĜĚĭĢįĞ 4ĮěĭĲĩĢħĠ
5P IFMQ XJUI UIF JOGFSFODF PG UIF SFTVMU UZQFT GPS BQQMJDBUJPOT BOE QSPKFDUJPOT XF QSPQPTF
B OFX TQFDJBMJ[FE TVCUZQJOH BMHPSJUIN GPS BQQMJDBUJPOT BOE QSPKFDUJPOT 4QFDJêDBMMZ DPOWFOUJPOBM TVCUZQJOH BMHPSJUINT UBLF UXP UZQFT BT JOQVUT BOE SFUVSO B CPPMFBO JOEJDBUJOHXIFUIFS UXP UZQFT BSF JO B TVCUZQJOH SFMBUJPO PS OPU 8F QSFTFOU BO BQQMJDBUJWF TVCUZQJOH BMHPSJUIN XIPTF JOUVJUJPO JT TJNQMF HJWFO B GVODUJPOBM UZQF A XIJDI NBZ CF BO JOUFSTFDUJPOPG GVODUJPOT BOE UIF UZQF PG BO BSHVNFOU B JU UFMMT XIFUIFS UIJT GVODUJPO DBO CF BQQMJFEUP UIJT BSHVNFOU BOE JG ZFT JU DPNQVUFT UIF PVUQVU UZQF 4JNJMBSMZ HJWFO B SFDPSE UZQF A
BOE B MBCFM l BQQMJDBUJWF TVCUZQJOH UFMMT XIFUIFS UIJT SFDPSE DBO CF QSPKFDUFE CZ UIJT MBCFM ,FZ *EFBT BOE $POUSJCVUJPOBOE JG ZFT JU DPNQVUFT UIF SFTVMU UZQF BTTPDJBUFE XJUI UIJT MBCFM #BTJDBMMZ XF USZ UP TPMWF UIFQSPCMFN JO UIF GPMMPXJOH TVCUZQJOH GPSN EFOPUFE BT <: XIFSF XF JOGFS UIF UZQF \ HJWFO
UIF BSHVNFOU UZQF AMi(AMi → ai`BM;)  ("QQH → ai`BM;) <: AMi →?
ѮJT QSPCMFN DBO CF TQMJU JOUP UXP TUFQT êSTU DIFDL XIFUIFS UIF BQQMJDBUJPO JT XFMMUZQFEBOE JG TP EFUFSNJOF JUT PVUQVU UZQF 'PS UIF BCPWF FYBNQMF \ JT FYQFDUFE UP CF ai`BM; BT AMi
JT BO BSHVNFOU UP AMi → ai`BM; 3FDPSE QSPKFDUJPO XPSLT TJNJMBSMZ ai`BM;  AMi TIPVME
CF EFSJWFE BT UIF SFTVMU UZQF GPS QSPKFDUJPO U&t 4 ]?2HHQ]'--&t 4 R'VXt
{x : ai`BM;}  {x : AMi} <: {x :?}"QQMJDBUJWF TVCUZQJOH JT VTFE XIFO UZQJOH BQQMJDBUJPOT BOE QSPKFDUJPOT 0VS BMHPSJUINBEPQUT UIF OPUJPO PG TFMFDUPST S UIBU BCTUSBDU UIF BSHVNFOUT BT B UZQF GPS BQQMJDBUJPOT PS B MB
CFM GPS QSPKFDUJPOT  ѮF CFIBWJPVS PG BQQMJDBUJWF TVCUZQJOH GPS JOUFSTFDUJPO UZQFT JT DBQUVSFECZ B TJNQMF DPNQPTJUJPO PQFSBUPS ! XIJDI JTPMBUFT QBSUJDVMBS EFTJHO DIPJDFT *O BQQMJDBUJWFTVCUZQJOH B QPTTJCMF SFTVMU JT UIBU UIF BQQMJDBUJPO GBJMT 8F EFOPUF GBJMVSF XJUI B . TZNCPM
8F JMMVTUSBUF UIF SFTVMUT PG BQQMJDBUJWF TVCUZQJOH EFOPUFE BT # GPS UIF BCPWF FYBNQMFT OFYUUAMi → ai`BM;V  U"QQH → ai`BM;V # AMi
4 ai`BM; ! X
Uai`BM; → AMiV  Uai`BM; → "QQHV # ai`BM; 4 AMi! "QQH&t , ai`BM;V
 &v , ai`BM;'# t
4 ai`BM; ! X&t , ai`BM;V &t ,AMi'# t
4 ai`BM; ! AMi"ĦěĢĮĠĮĢĭĢĞĬ 5P EFBM XJUI UIF BNCJHVJUJFT XF NFOUJPOFE JO UIF MBTU TFDUJPO XF JTPMBUFUIF CFIBWJPVS XIFO CPUI CSBODIFT DBO BDDFQU UIF TFMFDUPS UZQF 8F DBO SFKFDU PS BDDFQU UIFCFMPX DBTF XIFO XF BEPQU EJĒFSFOU DPNQPTJUJPO PQFSBUPST XIJDI XJMM CF FYQBOEFE JO UIF$IBQUFS (AMi → AMi)  (AMi → "QQH) # AMi = AMi ! "QQH.
"OPUIFS TPMVUJPO UP BWPJE BNCJHVJUJFT BOE SFDPWFS EFUFSNJOJTN JT UP BEPQU EJTKPJOU JOUFSTFDUJPO UZQFT XIJDI JT NFOUJPOFE JO UIF OFYU TFDUJPO BOE JT FYQMPSFE JO $IBQUFS $ĨīīĞĜĭħĞĬĬ 8F QSPWF UIF TPVOEOFTT BOE DPNQMFUFOFTT PG UIF BQQMJDBUJWF TVCUZQJOH XJUISFHBSE UP UIF OPSNBM TVCUZQJOH 8F IBWF TFWFSBM WBSJBOUT PG UIF NFUBUIFPSZ BOE POMZ TIPXUIF GVODUJPO DBTF IFSF ѮF EFUBJMT XJMM CF FYQBOEFE JO $IBQUFS -FNNB  4PVOEOFTT  *G A # B = C UIFO A <: B → C *OUSPEVDUJPO-FNNB  $PNQMFUFOFTT  *G A <: B → C UIFO ∃D, A # B = D ∧ D <: CϚϜϛ 5%04 ğĨī 0įĞīĥĨĚĝĢħĠ'PS UIF TFNBOUJDT XF GPMMPX VQ UIF JEFB PG UZQFEEJSFDUFE PQFSBUJPOBM TFNBOUJDT <)VBOH
FU BM > BOE EFêOF B OFX KVEHNFOU UIBU QFSGPSNT BQQMJDBUJWF EJTQBUDIJOH UP TVQQPSU PWFSMPBEJOH "U B IJHI MFWFM BQQMJDBUJWF EJTQBUDI SFëFDUT BQQMJDBUJWF TVCUZQJOH JO UIF EZOBNJDTFNBOUJDT "T XF BOBMZ[FE BCPWF EJTUSJCVUJWJUZ GPSCJET PWFSMPBEFE GVODUJPOT UP CF FYBDU
OFTUFE NFSHFT UIVT B DBOPOJDBM GPSN PG PWFSMPBEFE GVODUJPO TIPVME CF TFUUMFE 5P TPMWF UIJTQSPCMFN XF VTF BO FYQMJDJU NFSHF XJUI FYUSB BOOPUBUJPOT UIBU QMBZ B SPMF PG iSVOUJNF UZQFTu
XIJDI BSF VTFE CZ BQQMJDBUJWF EJTQBUDIJOH UP TFMFDU UIF DPSSFDU CSBODI EVSJOH SVOUJNF

ϚϜϜ 5İĨ $ĚĥĜĮĥĢ
8F QSFTFOU UXP DBMDVMJ UP EFNPOTUSBUF UIF BQQMJDBUJWF TVCUZQJOH BOE BQQMJDBUJWF EJTQBUDIJOHѮF êSTU DBMDVMVT FNCSBDFT B TJNQMF EFTJHO BOE BEPQUT BO VOSFTUSJDUFE NFSHF PQFSBUPS "MM
GFBUVSFT NFOUJPOFE BCPWF DBO CF FODPEFE JO UIJT DBMDVMVT CVU UIF DBMDVMVT XJMM IBWF B OPOEFUFSNJOJTUJD TFNBOUJDT EVF UP BNCJHVJUJFT 'PS BNCJHVJUJFT XF QSFTFOU B TFDPOE DBMDVMVTXIJDI BEPQUT B SFTUSJDUFE NFSHF PQFSBUPS POMZ UFSNT XJUI EJTKPJOU UZQFT DBO CF NFSHFE ѮJT
DBMDVMVT JT EFUFSNJOJTUJD CVU FYDMVEFT DFSUBJO GPSNT PG PWFSMPBEJOH MJLF UIF b?Qr GVODUJPO4JODF AMi → ai`BM; JT OPU EJTKPJOU XJUI "QQH → ai`BM; TVDI NFSHFT XJMM CF SFKFDUFEϚϜϝ 'ĢīĬĭĜĥĚĬĬ $ĮīīĢĞĝ 0įĞīĥĨĚĝĞĝ 'ĮħĜĭĢĨħĬ
'JSTUDMBTT DVSSJFE PWFSMPBEJOH JT DPOTJEFSFE B OPWFM GFBUVSF XIFO XF EFTJHOFE UIJT TZTUFN*U BQQFBST XIFO UIF TZTUFN IBT CPUI PWFSMPBEJOH BOE OFTUFE DPNQPTJUJPO BOE JT B QPXFSGVM
JEJPN XIFSF QSPHSBNNFST DBO BCTUSBDU PWFS BOE SFUVSO PWFSMPBEFE GVODUJPOT 'PS FYBNQMF
XF DSFBUF PVS PWFSMPBEFE GVODUJPO b?Qr CZ NFSHJOH UXP JNQMFNFOUBUJPOT UPHFUIFS Tb?Qr JT
UIF b?Qr GVODUJPO XSBQQFE JO B UIVOL
b?Qr , UAMi → ai`BM;V  U"QQH → ai`BM;Vb?Qr 4 b?QrAMi--b?Qr"QQH
Tb?Qr , lMBi → UAMi → ai`BM;V  U"QQH → ai`BM;V
Tb?Qr 4 λtX b?Qr

ѮF OFXMZ DSFBUFE GVODUJPO Tb?Qr JT TUJMM SFDPHOJTFE BT BO PWFSMPBEFE GVODUJPO JU NBLFT UIFTFMFDUJPO XIFO UIF TFDPOE BSHVNFOUT BSF HJWFO 8F TFF UIF FYBNQMFT CFMPXTb?Qr UV "→ b?Qr



Tb?Qr UV R "→ ]R]

Tb?Qr UV i`m2 "→ ]i`m2] 0VUMJOF BOE 1VCMJTIFE XPSL*O UIF MBTU UXP DBTFT XJUI B USBEJUJPOBM BQQSPBDI UP BQQMJDBUJPOT Tb?Qr JT FYQFDUFE UP IBWFUZQF lMBi → AMi → ai`BM; BOE lMBi → "QQH → ai`BM; SFTQFDUJWFMZ 'SPN UIF QFSTQFDUJWF PG JOUFSTFDUJPO PWFSMPBEJOH Tb?Qr TIPVME CF PG UZQF UlMBi → AMi → ai`BM;V UlMBi → "QQH → ai`BM;V XIJDI IPXFWFS JT EJĒFSFOU GSPN UIF HJWFO UZQF BOOPUBUJPOѮJT BMUFSOBUJWF WJFX PG UZQFT BOE GVODUJPOT NBLFT UIF PWFSMPBEFE GVODUJPOT ëFYJCMF UP QSPHSBN XJUIϚϜϞ 4ĮĦĦĚīĲ
*O TVNNBSZ UIF DPOUSJCVUJPOT PG UIJT UIFTJT BSFr $BMDVMJ TVQQPSUJOH PWFSMPBEJOH FYUFOTJCMF SFDPSET BOE OFTUFE DPNQPTJUJPO 8F QSPQPTF
DBMDVMJ XJUI JOUFSTFDUJPO UZQFT BOE B NFSHF PQFSBUPS XIJDI DBO TVQQPSU WBSJPVT GFBUVSFT UPHFUIFS VOMJLF QSFWJPVT DBMDVMJ XIFSF POMZ TPNF GFBUVSFT XFSF TVQQPSUFEr "QQMJDBUJWF TVCUZQJOH BOE EJTQBUDIJOH 8F EFWFMPQ B TQFDJBMJTFE BQQMJDBUJWF TVCUZQJOHSFMBUJPO UP EFBM XJUI UIF QSPCMFN PG JOGFSSJOH PVUQVU UZQFT GPS BQQMJDBUJPOT BOE SFDPSEQSPKFDUJPOT *O BEEJUJPO UIF EZOBNJD TFNBOUJDT TVQQPSUT B DPSSFTQPOEJOH BQQMJDBUJWFEJTQBUDIJOH SFMBUJPO
r 'JSTUDMBTT DVSSJFE PWFSMPBEJOH 8F TIPX UIBU UIF JOUFSBDUJPO CFUXFFO PWFSMPBEJOH BOE
OFTUFE DPNQPTJUJPO FOBCMFT PWFSMPBEFE GVODUJPOT UP CF êSTUDMBTT XIJDI BMMPXT UIFEFêOJUJPO PG DVSSJFE PWFSMPBEFE GVODUJPOTr *OUFSQSFUFS *NQMFNFOUBUJPO 8F JNQMFNFOU PVS DBMDVMVT BT B -JTQ EJBMFDU 8F FOSJDIUIF JNQMFNFOUBUJPO XJUI TFWFSBM QSJNJUJWFT BOE TZOUBDUJD TVHBS BOE FNQMPZ B DPOUSBDUCBTFE GVODUJPO UP FOTVSF UIF DPSSFDUOFTT PG UIF JOUFSQSFUFS
r .FDIBOJDBM GPSNBMJTBUJPO  "MM UIF TVCUZQJOH BMHPSJUINT DBMDVMJ BOE QSPPGT BSF GPSNBMJTFE JO UIF $PR UIFPSFN QSPWFSϚϝ 0ĮĭĥĢħĞ Ěħĝ 1ĮěĥĢĬġĞĝ İĨīĤѮJT UIFTJT JT PSHBOJTFE BT GPMMPXT
r $IBQUFS  HJWFT BO JOUSPEVDUJPO UP CBTJD DPODFQUT BOE OPUBUJPOBM QSFMJNJOBSJFT
r $IBQUFS  EJTDVTTFT BQQMJDBUJPO UZQJOH QSPCMFNT BOE DIBMMFOHFT BOE QSFTFOUT TFWFSBMBQQMJDBUJWF TVCUZQJOH EFTJHOT *OUSPEVDUJPOr $IBQUFS  QSFTFOUT UZQF TPVOE DBMDVMVT XJUI BO VOSFTUSJDUFE NFSHF PQFSBUPS XIJDI
TVQQPSUT BMM GFBUVSFT NFOUJPOFE QSFWJPVTMZ
r $IBQUFS  FOSJDI UIF QSFWJPVT DBMDVMVT XJUI EJTKPJOUOFTT BOE QSPWF JUT EFUFSNJOJTN
r $IBQUFS  HJWFT JOUFSQSFUFS JNQMFNFOUBUJPO PG PVS DBMDVMJ
r $IBQUFS  TIPXT UIF SFMBUFE XPSL BOE UIFJS EJĒFSFODFT
r $IBQUFS  DPODMVEFT UIJT UIFTJT BOE HJWFT EJSFDUJPOT GPS GVUVSF XPSL
1ĮěĥĢĜĚĭĢĨħĬ ѮJT UIFTJT JT QBSUJBMMZ CBTFE PO UIF CFMPX QVCMJDBUJPOT
9V 9VF #SVOP $ E 4 0MJWFJSB BOE /JOHOJOH 9JF i"QQMJDBUJWF *OUFSTFDUJPO5ZQFTu *O ćF UI "TJBO 4ZNQPTJVN PO 1SPHSBNNJOH -BOHVBHFT BOE 4ZTUFNT"1-"4  "īĭĢğĚĜĭ ѮF NFDIBOJDBM GPSNBMJTBUJPO BOE JOUFSQSFUFS JNQMFNFOUBUJPO DBO CF GPVOE BU
?iiTb,ff;Bi?m#X+QKfDmMBQ`ttm2fTTHB+iBp2@BMi2`b2+iBQMϛ #ĚĜĤĠīĨĮħĝ*O UIJT DIBQUFS CBTJD DPODFQUT BOE OPUBUJPOBM QSFMJNJOBSJFT XJMM CF FYQMBJOFE JO EFUBJM ѮJT
QBSU JT IFMQGVM GPS SFBEFST UP HBJO TPNF JOUVJUJPO BOE SFGFSFODFT JO PSEFS UP CFUUFS VOEFSTUBOE
BOE FWBMVBUF UIF SFTU PG UIF UIFTJT 4FDUJPO  JOUSPEVDFT UIF 4JNQMZ 5ZQFE λ$BMDVMVT BOEUIF OPUJPO PG TVCUZQJOH UIFO EJTDVTTFT UIFJS DPNCJOBUJPO XJUI CJEJSFDUJPOBM UZQJOH λ≤ 
4FDUJPO  FYQMBJOT JOUFSTFDUJPO UZQFT UIF NFSHF PQFSBUPS BOE UIFJS BQQMJDBUJPOT 4FDUJPO QSFTFOUT B DBMDVMVT JOUSPEVDFE CZ %VOêFME XIJDI TFSWFT BT B TUBSUJOH QPJOU PG PVS TZTUFN
4FDUJPO  JOUSPEVDFT UIF NBJO JEFB PG UZQFEJSFDUFE PQFSBUJPOBM TFNBOUJDTϛϚ 4ĢĦĩĥĲ 5ĲĩĞĝ λ$ĚĥĜĮĥĮĬ İĢĭġ 4ĮěĭĲĩĢħĠ
ѮF λ$BMDVMVT JT B GPSNBMJTBUJPO PG B NBUIFNBUJDBM NPEFM UIBU EFTDSJCFT DPNQVUBUJPO *U
IBT JOTQJSFE UIF EFTJHOT PG NBOZ NBJOTUSFBN QSPHSBNNJOH MBOHVBHFT 1ZUIPO +BWB4DSJQU
FUD BOE IBT BMTP CFFO BEPQUFE BT UIF CBTJT PG GVODUJPOBM QSPHSBNNJOH MBOHVBHFT TVDI BT
4DIFNF )BTLFMM FUDϛϚϚ 4ĢĦĩĥĲ 5ĲĩĞĝ λ$ĚĥĜĮĥĮĬ
ѮF QSPUPUZQF PG UIF λ$BMDVMVT XBT êSTUMZ JOUSPEVDFE CZ $IVSDI <> UP TFSWF BT UIF GPVOEBUJPO PG NBUIFNBUJDT *UT JODPOTJTUFODZ XBT QPJOUFE PVU CZ ,MFFOF BOE 3PTTFS <> -BUFS$IVSDI SFWJTFE JU JOUSPEVDFE VOUZQFE λ$BMDVMVT BOE UIFO BVHNFOUFE JU XJUI UZQFT UP NBLF
JU CFDPNF MPHJDBMMZ DPOTJTUFOU <$IVSDI > ѮF λ$BMDVMVT XJUI TJNQMF UZQFT CBTF UZQFTBOE BSSPX UZQFT JT DBMMFE UIF 4JNQMZ 5ZQFE λ$BMDVMVT 45-$ ѮF VTBHF PG UZQFT EFWFMPQT JOUP UIF EFTJHO PG UIF UZQF TZTUFN XIFSF UIF NPTU GVOEBNFOUBM
QSPQFSUZ JT UZQF TBGFUZ EFTDSJCFE CZ .JMOFS <>
8FMMUZQFE QSPHSBNT DBOOPU iHP XSPOHu 
1SBDUJDBMMZ UZQF TBGFUZ  FOTVSFT UIBU UIF UZQFDIFDLFS XJMM EFUFDU BMM TUVDL UFSNT CFGPSFUIF FWBMVBUJPO *O 45-$ XFMMUZQFE QSPHSBNT BSF FYQSFTTJPOT XIJDI DBO CF UZQFDIFDLFE

i8SPOHu EPFT OPU NFBO UIBU XF DBO FYDMVEF BMM CBE DBTFT POMZ QBSU PG UIFN MJLF BEE BO JOUFHFS UP B TUSJOH
1FPQMF VTVBMMZ USFBU UZQF TBGFUZ BOE UZQF TPVOEOFTT BT TZOPOZNT CVU GPS DMBSJUZ XF POMZ VTF UZQF TPVOEOFTTUP EFTDSJCF UIF UIFPSFN UIBU DBO CF GPSNBMMZ TUBUFE BOE QSPWFE #BDLHSPVOE
5FSNT JO UIF λ$BMDVMVT BSF MJUFSBMT WBSJBCMFT BCTUSBDUJPOT BOE BQQMJDBUJPO 5ZQFT BSF MJUFSBMUZQFT BOE BSSPX UZQFT BMTP DBMMFE GVODUJPO UZQFT  " DPOUFYU JT B TFRVFODF PG QBJST CFUXFFOWBSJBCMFT BOE UIFJS UZQFT&YQSFTTJPOT
5ZQFT$POUFYU

e

:=

A, B

:=

Γ

:=

i | x | λx : A. e | e1 e2
Int | A → B∅ | Γ, x : A*O TZOUBY
r i JT VTFE GPS MJUFSBMT GPS TJNQMJDJUZ XF POMZ DPOTJEFS JU BT OVNCFSTr λ JT PѫFO VTFE GPS UIF QSFêY OBNF PG B DBMDVMVT PS B MBNCEB BCTUSBDUJPO JO UIF λ$BMDVMVT
r x, y, z BSF SFTFSWFE GPS CPVOE WBSJBCMFT JO UIF λ$BMDVMVTr A, B, C BSF SFTFSWFE GPS UZQF WBSJBCMFT
r ei JT VTFE GPS UFSNTr Γ EFTDSJCFT B UZQJOH DPOUFYU XIJDI JT B TFRVFODF PG QBJST (x, A)
8JUI UIF TZOUBY PG FYQSFTTJPOT UZQFT BOE DPOUFYU EFêOFE XF XJMM JOUSPEVDF B SFMBUJPODBMMFE UZQJOH BTTJHONFOU JO 'JHVSF  XIJDI JT B BSZ SFMBUJPO CFUXFFO DPOUFYU Γ UFSN e
BOE UZQF A 3VMF 5-Ģĭ TUBUFT UIBU MJUFSBMT IBWF JOUFHFS UZQFT 3VMF 57Ěī TBZT UIBU WBSJBCMF
x IBT UIF UZQF A JG UIF DPOUFYU Γ IBT UIFJS BTTPDJBUJPO 3VMF 5-ĚĦ JT UIF SVMF GPS MBNCEBBCTUSBDUJPOT λx : A. e IBT UIF BSSPX UZQF A → B JG UIF CPEZ e IBT UIF UZQF B VOEFS UIFDPOUFYU Γ FYUFOEFE XJUI B QBJS x : A ѮF BQQMJDBUJPO SVMF 5"ĩĩ EFSJWFT UIF PVUQVU UZQF
GSPN e1 BOE DIFDLT UIF FRVBMJUZ CFUXFFO UIF JOQVU UZQF BOE UIF UZQF PG BSHVNFOU e2  8JUIUIF UZQJOH SVMFT XF XJMM SFKFDU JMMUZQFE UFSNT MJLF 1 2 MJUFSBM  JT BQQMJFE UP BSHVNFOU  TJODF
1 EPFT OPU IBWF B GVODUJPO UZQF
ѮF UZQJOH BTTJHONFOU SFMBUJPO EFêOFT UIF TUBUJDT PG UIF MBOHVBHF XIJMF TFNBOUJDT EFêOFT
JUT EZOBNJDT ѮFSF BSF NBOZ BQQSPBDIFT UP EFêOF TFNBOUJDT JODMVEJOH EFOPUBUJPOBM TFNBOUJDT <4DINJEU > PQFSBUJPOBM TFNBOUJDT <1MPULJO > BOE BYJPNBUJD TFNBOUJDT <(PHVFO
FU BM > ѮJT UIFTJT POMZ GPDVTFT PO PQFSBUJPOBM TFNBOUJDT TJODF JU JT DMPTFS UP UIF DPNQVUBUJPO JOUVJUJPO BOE JNQMFNFOUBUJPO EFUBJMT#FGPSF QSFTFOUJOH UIF SFEVDUJPO SVMFT PG UIF PQFSBUJPOBM TFNBOUJDT UIF OPSNBM GPSN PG UIJTMBOHVBHF TIPVME CF FTUBCMJTIFE UP DIBSBDUFSJTF UIF FOE PG UIF DPNQVUBUJPO QSPDFTT 3FEVDJCMF
UFSNT BSF DBMMFE SFEFYFT "O FYQSFTTJPO DPOUBJOJOH OP SFEFYFT JT JO OPSNBM GPSN ѮF OPSNBM

 4JNQMZ 5ZQFE λ$BMDVMVT XJUI 4VCUZQJOH
5ZQJOH

Γ'e:A
5-Ģĭ

Γ ' J : AMi

57Ěī

5-ĚĦ

Γ'Y:A

Γ ' λY : A. e : A → B

Γ, Y : A ' e : B

x:A∈Γ

5"ĩĩ

Γ ' e : A → B

Γ ' e : A

Γ ' e e : B'JHVSF  45-$ 5ZQJOH

4NBMM4UFQ 3FEVDUJPOe )−→ e"45#ĞĭĚ

(λY : A. e) v )−→ e[Y )→ v]

45"ĩĩ-45"ĩĩ3e e )−→ e" ev e )−→ v e"e )−→ e"

e )−→ e"

'JHVSF  45-$ 0QFSBUJPOBM 4FNBOUJDTGPSN EFêOFT UIF QPTTJCMF TUSVDUVSF PG UFSNJOBUJPO PG SFEVDUJPO XIJDI JT SFQSFTFOUFE CZ WBMVF
VOEFS UIF DPOUFYU PG PQFSBUJPOBM TFNBOUJDT " WBMVF JT FJUIFS B MJUFSBM PS B MBNCEB BCTUSBDUJPOJO UIF 45-$
7BMVFTv := i | λx : A. e

*O 'JHVSF  SVMF 45"ĩĩ- BOE SVMF 45"ĩĩ3 BSF OPSNBM DPOHSVFODF SVMFT BOE BDDPVOUGPS FWBMVBUJOH UIF BSHVNFOUT CFGPSF UIFZ BSF TVCTUJUVUFE JO UIF BCTUSBDUJPO CPEZ " NPSFJOUFSFTUJOH SVMF JT SVMF 45#ĞĭĚ XIJDI JOUSPEVDFT B OFX PQFSBUJPO TVCTUJUVUJPO 4VCTUJUVUJPOFTTFOUJBMMZ EFTDSJCFT TVCTUJUVUJOH POF FYQSFTTJPO GPS B WBSJBCMF JO BOPUIFS FYQSFTTJPO %FBMJOH
XJUI DBQUVSFBWPJEJOH TVCTUJUVUJPO PѫFO JOWPMWFT DVNCFSTPNF SFBTPOJOH XF XJMM VTF UIFUFDIOJRVF PG -PDBMMZ /BNFMFTT 3FQSFTFOUBUJPO <$IBSHVÊSBVE > GPS UIF GPSNBMJTBUJPO PG
PVS DBMDVMJ JO $PRϛϚϛ 4ĮěĭĲĩĢħĠ
4VCUZQJOH BSJTFT BT POF PG UIF DSJUJDBM GFBUVSFT JO 0CKFDU0SJFOUFE 1SPHSBNNJOH *U EFTDSJCFTUIF CFIBWJPVS PѫFO DBMMFE TVCUZQF QPMZNPSQIJTN UIBU UFSNT DBO CF TBGFMZ SFQMBDFE CZ PUIFS #BDLHSPVOE
4VCUZQJOH

A≤B
43Ğğĥ

A≤A

45īĚħĬ

A≤B

4"īī

B≤C

B  ≤ AA≤CA ≤ B A → A ≤ B  → B 

45Ĩĩ

A ≤ hQT'JHVSF  45-$ 4VCUZQJOHUFSNT UZQFE XJUI UIFJS TVCUZQF 3FëFDUJOH PO UIF UZQJOH SFMBUJPO XPVME CF UIF UZQJOH TVCTVNQUJPO SVMF
5Ĳ4Įě

Γ'e:A

A≤B

Γ'e:B
3VMF 5Ĳ4Įě TBZT UIBU JG e IBT UIF UZQF A BOE A JT UIF TVCUZQF PG B UIFO e IBT UIF UZQF BѮF JOUVJUJPO UP VOEFSTUBOE UIF TVCTVNQUJPO JT UP UIJOL PG JU BT UIF GFBUVSF PG PCKFDUPSJFOUFEQSPHSBNNJOH XIFSF UIF UFSN UZQFE XJUI B TVCDMBTT DBO BMTP IBWF UIF TVQFSDMBTT UZQF 8F
GPSNBMMZ EFêOF UIF TVCUZQJOH JO 'JHVSF  A ≤ B JT UIF TVCUZQJOH SFMBUJPO XIJDI DBO CF
WJFXFE BT B QSFPSEFS PG TFUT PG UXP UZQFT

3VMF 4Įě3Ğğĥ BOE SVMF 4Įě5īĚħĬ EFêOF UIF QSPQFSUJFT PG SFëFYJWJUZ BOE USBOTJUJWJUZ
3VMF 4"īī EFTDSJCFT UIF TVCUZQJOH SFMBUJPO PG BSSPX UZQFT JOQVU UZQFT BSF DPOUSBWBSJBOUBOE PVUQVU UZQFT BSF DPWBSJBOU 3VMF 45Ĩĩ FNQMPZT B OFX hQT UZQF XIJDI JT UIF TVQFSUZQF
PG BMM UZQFTϛϚϜ #ĢĝĢīĞĜĭĢĨħĚĥ 5ĲĩĢħĠ*OJUJBMMZ B UZQJOH KVEHNFOU POMZ BDDPVOUT GPS B UZQF BTTJHONFOU TZTUFN XIJDI JT PѫFO XSJUUFOJO UIF GPSN PG
Γ'e:A#JEJSFDUJPOBM UZQJOH JOUSPEVDFT B OPUJPO PG NPEF <8BSSFO > JOUP UZQJOH TZOUIFTJT NPEF
BOE DIFDL NPEF
r 4ZOUIFTJT .PEF ⇒  4ZOUIFTJ[F B UZQF GSPN BO FYQSFTTJPO XIJDI DBO CF JNQMFNFOUFEBT B JOGFS GVODUJPO XJUI UZQJOH DPOUFYU Γ BOE FYQSFTTJPO e BT JOQVUT BOE UIF UZQF A BT
PVUQVU 4JNQMZ 5ZQFE λ$BMDVMVT XJUI 4VCUZQJOH#JEJSFDUJPOBM 5ZQJOH

Γ'e⇔A
5Ĳ-Ģĭ

Γ ' e ⇒ A → B

5Ĳ-ĚĦ

Γ'Y⇒A

Γ ' λY : A. e ⇒ A → B

Γ, Y : A ' e ⇒ B

x:A∈ΓΓ ' J ⇒ AMi
5Ĳ"ĩĩ

5Ĳ7Ěī

Γ ' e ⇐ A

Γ ' e e ⇒ B

5Ĳ"ħħ

Γ'e⇐A

Γ'e:A⇒A

5Ĳ4Įě

Γ'e⇒A

A≤B

Γ'e⇐B

'JHVSF  #JEJSFDUJPOBM 5ZQJOH

r $IFDL .PEF ⇐  $IFDL BO FYQSFTTJPO XJUI B TQFDJêD UZQF XIJDI DBO CF JNQMFNFOUFEBT B DIFDL GVODUJPO XJUI UZQJOH DPOUFYU Γ UIF FYQSFTTJPO e BOE UIF UZQF A BT JOQVUTBOE CPPMFBOT JOEJDBUJOH TVDDFTT PS GBJMVSF BT PVUQVU#JEJSFDUJPOBM UZQJOH PSJHJOBUFE GSPN 1JFSDF BOE 5VSOFS <> BOE JT FYUSFNFMZ IFMQGVM
GPS UZQJOH B TZTUFN XJUI TVCUZQJOH CZ BEEJOH UZQF BOOPUBUJPOT ѮF UZQJOH PG 45-$ XJUITVCUZQJOH DBO CF JOUSPEVDFE CZ CJEJSFDUJPOBMJ[JOH FBDI SVMF JO 'JHVSF  ѮFSF BSF UXPSVMFT UP USJHHFS UIF DIFDL NPEF SVMFT 5Ĳ"ĩĩ BOE 5Ĳ"ħħ 3VMF 5Ĳ"ĩĩ FYQFDUT e1 UP JOGFSUIF BSSPX UZQF BOE VTF UIF JOQVU UZQF A UP DIFDL UIF BSHVNFOU e2  3VMF 5Ĳ"ħħ VTFT UIFBOOPUBUFE UZQF UP DIFDL UIF UFSN e
*O DPODMVTJPO UIFSF BSF TFWFSBM BEWBOUBHFT PG CJEJSFDUJPOBM UZQJOH
r *U JT FBTZ UP FYUFOE UIF UZQF TZTUFN UP TVQQPSU TVCUZQJOH
r ѮF GFBUVSF PG MPDBM UZQF JOGFSFODF FOBCMFT TJNQMFS TZOUBY BOE MPDBMJTFT UIF FSSPS JOGPSNBUJPOϛϚϝ .ĞĭĚĭġĞĨīĲ*O UIF TFUUJOH PG PQFSBUJPOBM TFNBOUJDT UZQF TPVOEOFTT DBO CF EFUFSNJOFE CZ QSFTFSWBUJPOBOE QSPHSFTT <8SJHIU BOE 'FMMFJTFO > ѮFSF BSF UISFF QSPQFSUJFT XF BSF JOUFSFTUFE JOćFPSFN  1SFTFSWBUJPO  *G ∅ ' e : A BOE e )−→ e" UIFO ∅ ' e" : A
1SFTFSWBUJPO UFMMT UIBU UIF UZQF PG FYQSFTTJPO XJMM CF QSFTFSWFE EVSJOH UIF FWBMVBUJPO ѮJT JT
OPU UIF DBTF XIFO UIFSF JT TVCUZQJOH XIFSF UIF UZQF NBZ CFDPNF TNBMMFS 8F DBO TMJHIUMZNPEJGZ UIJT UIFPSFN JO UIF QSFTFODF PG TVCUZQJOH
ćFPSFN  1SFTFSWBUJPO  *G ∅ ' e : A BOE e )−→ e" UIFO ∃B ∅ ' e" : B BOE B ≤ A #BDLHSPVOEćFPSFN  1SPHSFTT  *G e JT XFMMUZQFE UIFO e JT B WBMVF PS ∃e" , e )−→ e" ѮF QSPHSFTT UIFPSFN FOTVSFT UIBU BOZ XFMMUZQFE FYQSFTTJPO JT FJUIFS B WBMVF PS NBLFT B
QSPHSFTTćFPSFN  %FUFSNJOJTN  *G e JT XFMMUZQFE e )−→ e1 BOE e )−→ e2 UIFO e1 = e2 
%FUFSNJOJTN JT B TUSPOH QSPQFSUZ XIJDI SFRVJSFT FBDI SFEVDUJPO TUFQ JT EFUFSNJOJTUJDϛϛ *ħĭĞīĬĞĜĭĢĨħ 5ĲĩĞĬ Ěħĝ .ĞīĠĞ 0ĩĞīĚĭĨī
8F IBWF BMSFBEZ TFFO POF DPNQPVOE UZQF JO 45-$ BSSPX UZQFT *O UIJT TFDUJPO XF JOUSPEVDFBOPUIFS POF JOUFSTFDUJPO UZQFT 8F UIFO JOUSPEVDF UIF NFSHF PQFSBUPS XIJDI JT BCMF UPDSFBUF UFSNT JOIBCJUFE CZ JOUFSTFDUJPO UZQFTϛϛϚ *ħĭĞīĬĞĜĭĢĨħ 5ĲĩĞĬ*OUFSTFDUJPO UZQFT EFOPUFE BT A  B XFSF êSTUMZ JOUSPEVDFE JO $PQQP FU BM <> BT BUIFPSFUJDBM OPUJPO UP EFTDSJCF UIF QSPQFSUJFT PG λ UFSNT 4JNQMZ TQFBLJOH JOUFSTFDUJPO UZQFTFOBCMF POF UFSN UP IBWF NVMUJQMF UZQFT "T QSFTFOUFE JO UZQJOH SVMFT B UFSN e DBO IBWF UIFJOUFSTFDUJPO UZQFT JG e IBT CPUI UIF UZQF A BOE UIF UZQF Bó*ħĭīĨ

Γ'e:A

Γ'e:B

Γ'e:ABó&ĥĢĦ-ó&ĥĢĦ3

Γ'e:AB

Γ'e:AB

Γ'e:A

Γ'e:B

*G UZQFT BSF USFBUFE BT B XBZ UP EFTDSJCF TFUT PG UFSNT UIFO JOUFSTFDUJPO UZQFT BSF JOUSPEVDFEUP EFTDSJCF DPOKVODUJWF GPSNT $BMDVMJ XJUI JOUFSTFDUJPO UZQFT XJMM IBWF NBOZ JOUFSFTUJOHQSPQFSUJFT 'PS FYBNQMF UIFZ DBO UZQF DIFDL UFSNT XIJDI BSF JNQPTTJCMF UP CF DIFDLFE CZ
TJNQMF UZQFT ѮF TFMGBQQMJDBUJPO UFSN λx : A  (A → B). x x DBOOPU CF UZQFE JO 45-$
CVU JU JT B XFMMUZQFE UFSN JO DBMDVMJ XJUI JOUFSTFDUJPO UZQFT"MUIPVHI JU JT NFBOJOHMFTT UP êOE TPNF UFSNT XIJDI JT UIF JOUFSTFDUJPO PG JOUFHFST BOE
CPPMFBOT UIJOHT XJMM CFDPNF NPSF JOUFSFTUJOH XIFO XF DSFBUF JOUFSTFDUJPO UZQFT PG NPSF
DPNQMFY UFSNT FH GVODUJPOT SFDPSET BOE JOUFSGBDFT  *OUFSTFDUJPO UZQFT IBWF BMSFBEZ CFFOBEPQUFE CZ NBOZ QSPHSBNNJOH MBOHVBHFT JODMVEJOH 5ZQF4DSJQU 4DBMB FUDϛϛϛ .ĞīĠĞ 0ĩĞīĚĭĨī
ѮF NFSHF PQFSBUPS EFOPUFE BT , , IBT CFFO JOUSPEVDFE CZ 3FZOPMET <3FZOPMET > BOE
MBUFS SFêOFE CZ %VOêFME <%VOêFME > UP DSFBUF UFSNT XJUI JOUFSTFDUJPO UZQFT BU UIF UFSN *OUFSTFDUJPO 5ZQFT BOE .FSHF 0QFSBUPSMFWFM "O JNQPSUBOU GFBUVSF PG %VOêFMET DBMDVMVT JT UIBU JU DPOUBJOT B DPNQMFUFMZ VOSFTUSJDUFE
NFSHF PQFSBUPS XIJDI FOBCMFT NPTU PG UIF BQQMJDBUJPOT UIBU XF XJMM EJTDVTT JO UIJT UIFTJT FYDFQU GPS OFTUFE DPNQPTJUJPO )PXFWFS UIJT FYQSFTTJWF QPXFS DPNFT BU B DPTU ѮF TFNBOUJDTPG UIF DBMDVMVT JT BNCJHVPVT 'PS FYBNQMF R--k , AMi DBO FMBCPSBUF UP CPUI R BOE k /PUF
UIBU JOUFSTFDUJPO UZQFT JO UIF QSFTFODF PG UIF NFSHF PQFSBUPS IBWF B EJĒFSFOU JOUFSQSFUBUJPOGSPN UIF PSJHJOBM NFBOJOH <$PQQP FU BM > XIFSF UZQF JOUFSTFDUJPOT A  B BSF POMZJOIBCJUFE CZ UIF JOUFSTFDUJPO PG UIF TFUT PG WBMVFT PG A BOE B *O HFOFSBM XJUI UIF NFSHF
PQFSBUPS XF DBO BMXBZT êOE B UFSN GPS BOZ JOUFSTFDUJPO UZQF FWFO XIFO UIF UXP UZQFT JO UIFJOUFSTFDUJPO BSF EJTKPJOU JF XIFO UIF TFUT PG WBMVFT EFOPUFE CZ UIF UXP UZQFT BSF EJTKPJOU 'PS FYBNQMF R--i`m2 IBT UIF UZQF AMi  "QQH *O NBOZ DMBTTJDBM JOUFSTFDUJPO UZQF TZTUFNTXJUIPVU UIF NFSHF PQFSBUPS TVDI UZQF XPVME OPU CF JOIBCJUFE <1PUUJOHFS > ѮVT UIFVTF PG UIF UFSN iJOUFSTFDUJPOu JT NFSFMZ B IJTUPSJDBM MFHBDZ ѮF NFSHF PQFSBUPS BEET FYQSFTTJWF QPXFS UP DBMDVMJ XJUI JOUFSTFDUJPO UZQFT "T XF TIBMM TFF UIJT BEEFE FYQSFTTJWF QPXFS JTVTFGVM UP NPEFM TFWFSBM GFBUVSFT PG QSBDUJDBM JOUFSFTU GPS QSPHSBNNJOH MBOHVBHFTϛϛϜ "ĩĩĥĢĜĚĭĢĨħĬ Ĩğ .ĞīĠĞ 0ĩĞīĚĭĨī
5P TIPX UIBU UIF NFSHF PQFSBUPS JT VTFGVM XF OPX DPWFS GPVS BQQMJDBUJPOT PG UIF NFSHF PQFSBUPS UIBU IBWF BQQFBSFE JO UIF MJUFSBUVSF SFDPSET BOE SFDPSE QSPKFDUJPOT GVODUJPO PWFSMPBEJOH SFUVSO UZQF GVODUJPO PWFSMPBEJOH BOE OFTUFE DPNQPTJUJPO "MM BQQMJDBUJPOT DBO BMM
CF FODPEFE CZ PVS DBMDVMVT JO $IBQUFS 
3ĞĜĨīĝĬ Ěħĝ 3ĞĜĨīĝ 1īĨģĞĜĭĢĨħĬ ѮF JEFB PG VTJOH UIF NFSHF PQFSBUPS UP NPEFM SFDPSEDPODBUFOBUJPO êSTUMZ BQQFBST JO 3FZOPMET <> 3FDPSET JO PVS DBMDVMJ BSF NPEFMMFE BT
NFSHFT PG NVMUJQMF TJOHMFêFME SFDPSET .VMUJêFME SFDPSET DBO CF WJFXFE BT TZOUBDUJD TVHBS
BOE &t 4 ]?2HHQ]- v 4 ]rQ`H/]' JT TJNQMZ U&t 4 ]?2HHQ'--&v 4 ]rQ`H/]'V ѮF CFIBWJPVS PG SFDPSE QSPKFDUJPO JT NPTUMZ TUBOEBSE JO PVS DBMDVMJ "ѫFS CFJOH QSPKFDUFE CZ B
MBCFM UIF NFSHFE SFDPSET XJMM SFUVSO UIF BTTPDJBUFE UFSNT 'PS JOTUBODF "→ EFOPUFT SFEVDF
UP ({t = ]?2HHQ]}, , {v = ]rQ`H/]}).t "→ ]?2HHQ]'ĮħĜĭĢĨħ ĨįĞīĥĨĚĝĢħĠ 'VODUJPO PWFSMPBEJOH JT B GPSN PG QPMZNPSQIJTN XIFSF UIF JN
QMFNFOUBUJPO PG GVODUJPOT DBO WBSZ EFQFOEJOH PO UIF EJĒFSFOU UZQFT PG BSHVNFOUT UIBU BSF
BQQMJFE CZ GVODUJPOT ѮFSF BSF NBOZ XBZT UP SFQSFTFOU UZQFT PG PWFSMPBEFE GVODUJPOT 'PS
FYBNQMF TVQQPTF b?Qr JT BO PWFSMPBEFE GVODUJPO UIBU DBO CF BQQMJFE UP FJUIFS JOUFHFST PS
CPPMFBOT )BTLFMM VUJMJTFT UZQF DMBTTFT <8BEMFS BOE #MPUU > UP BTTJHO UIF UZQF a?Qr  ⇒ → ai`BM; UP b?Qr XJUI JOTUBODFT EFêOFE

 #BDLHSPVOE
8JUI JOUFSTFDUJPO UZQFT XF DBO FNQMPZ UIF NFSHF PQFSBUPS <$BTUBHOB FU BM  3FZOPMET
> UP EFêOF B TJNQMJêFE WFSTJPO PG UIF PWFSMPBEFE b?Qr GVODUJPO 'PS JOTUBODF UIF b?Qr
GVODUJPO CFMPX IBT UZQF UAMi → ai`BM;V  U"QQH → ai`BM;Vb?Qr : (AMi → ai`BM;)  ("QQH → ai`BM;) = b?QrAMi--b?Qr"QQH
ѮF CFIBWJPVS PG b?Qr JT TUBOEBSE BDUJOH BT B OPSNBM GVODUJPO JU DBO CF BQQMJFE UP BSHVNFOUT BOE UIF DPSSFDU JNQMFNFOUBUJPO JT TFMFDUFE CBTFE PO UZQFT
b?Qr R "→ R

b?Qr i`m2 "→ ]i`m2]3ĞĭĮīħ ĭĲĩĞ ĨįĞīĥĨĚĝĢħĠ 0OF DPNNPO FYBNQMF PG SFUVSO UZQF PWFSMPBEJOH JT UIF `2/
GVODUJPO JO )BTLFMM`2/ :: _2/  ⇒ ai`BM; → 
XIJDI JT UIF SFWFSTF PQFSBUJPO PG b?Qr BOE QBSTFT B TUSJOH JOUP TPNF PUIFS GPSN PG EBUB -JLF
b?Qr XF DBO EFêOF B TJNQMJêFE WFSTJPO PG `2/ VTJOH UIF NFSHF PQFSBUPS

`2/ : (ai`BM; → AMi)  (ai`BM; → "QQH) = `2/AMi--`2/"QQH*O )BTLFMM CFDBVTF UIF SFUVSO UZQF  DBOOPU CF EFUFSNJOFE CZ UIF BSHVNFOU `2/ FJUIFSSFRVJSFT QSPHSBNNFST UP HJWF BO FYQMJDJU UZQF BOOPUBUJPO PS OFFET UP BVUPNBUJDBMMZ JOGFS UIFSFUVSO UZQF GSPN UIF DPOUFYU 0VS DBMDVMJ XPSL JO B TJNJMBS NBOOFS 4VQQPTF bm++ JT UIFTVDDFTTPS GVODUJPO PO JOUFHFST BOE MQi JT UIF OFHBUJPO GVODUJPO PO CPPMFBOT UIFO XF DBO
XSJUF
bm++ (`2/ ]R]) "→ kMQi (`2/ ]i`m2]) "→ 7Hb2/ĞĬĭĞĝ $ĨĦĩĨĬĢĭĢĨħ 4JNQMZ TUBUFE OFTUFE DPNQPTJUJPO SFëFDUT EJTUSJCVUJWJUZ QSPQFSUJFTPG JOUFSTFDUJPO UZQFT BU UIF UFSN MFWFM 8IFO FMJNJOBUJOH UFSNT DSFBUFE CZ UIF NFSHF PQFSBUPSVTVBMMZ GVODUJPOT BOE SFDPSET UIF SFTVMUT FYUSBDUFE GSPN OFTUFE UFSNT XJMM CF DPNQPTFE *O
UIF DPOUFYU PG SFDPSET UIF EJTUSJCVUJWF TVCUZQJOH SVMF FOBCMJOH UIJT CFIBWJPVS JT {l : A}  {l :B} <: {l : A  B} 8JUI UIJT SVMF XF DBO IBWF UIF GPMMPXJOH FYQSFTTJPO
({t 4 ]?2HHQ]}--{t 4 R}).t "→ ]?2HHQ]--R/PUF UIBU IFSF XF BMMPX SFQFBUFE êFMET XJUI UIF TBNF OBNF 0OF NBZ XPSSZ BCPVU BNCJHVJUJFT CVU XJUI B EJTKPJOUOFTT SFTUSJDUJPO XF DBO POMZ BDDFQU êFMET XJUI UIF TBNF MBCFMTJG UIF UZQFT PG UIF êFMET BSF EJTKPJOU /FTUFE DPNQPTJUJPO JT B LFZ GFBUVSF JO DPNQPTJUJPOBM %VOĕFMET $BMDVMVTQSPHSBNNJOH <;IBOH FU BM > XIJDI VTFT JU UP TPMWF DIBMMFOHJOH NPEVMBSJUZ QSPCMFNTTVDI BT UIF &YQSFTTJPO 1SPCMFN <8BEMFS > BOE UP NPEFM GPSNT PG GBNJMZ QPMZNPSQIJTN<&SOTU > 8F SFGFS JOUFSFTUFE SFBEFST UP UIF XPSL PG ;IBOH FU BM <> GPS EFUBJMT/FTUFE DPNQPTJUJPO DBO BMTP PDDVS XJUI GVODUJPOBM JOUFSTFDUJPOT VTJOH UIF TVCUZQJOH SVMF
(A → B)  (A → C) <: A → (B  C) 8JUI UIJT SVMF XF DBO GPS FYBNQMF XSJUF UIFGPMMPXJOH FYQSFTTJPO

(bm++--BMihQ.B;Bi) 8 "→ e--]8]
XIJDI BQQMJFT UXP GVODUJPOT UP UIF JOUFHFS 8 /PUF UIBU IFSF BMihQ.B;Bi UBLFT BO JOUFHFS
BOE SFUVSOT B DPSSFTQPOEJOH DIBSBDUFS 8F XJMM BMTP TFF UIBU OFTUFE DPNQPTJUJPO FOBCMFTPWFSMPBEFE GVODUJPOT UP CF DVSSJFEϛϜ %ĮħğĢĞĥĝĬ $ĚĥĜĮĥĮĬ*O UIJT TFDUJPO XF XJMM HJWF BO JOUSPEVDUJPO UP %VOêFMET DBMDVMVT <%VOêFME > XIJDI
BJNT UP QSPWJEF B HFOFSBM NFDIBOJTN UP TVCTVNF EJĒFSFOU GFBUVSFT JODMVEJOH PWFSMPBEJOHSFDPSET BOE IFUFSPHFOFPVT EBUB *O IFS DBMDVMVT JOUFSTFDUJPO UZQFT BOE NFSHF PQFSBUPS BSF
JOUSPEVDFE JO UIF TZOUBY 'PS TJNQMJDJUZ XF JHOPSF UIF VOJPO UZQFT IFSFϛϜϚ 4ĲħĭĚı
8F êSTU QSFTFOU UIF TPVSDF TZOUBY PG UIF DBMDVMVT&YQSFTTJPOT

e

:=

A, B

:=

$POUFYUΓ:=

7BMVFT

v

:=

5ZQFT

() | x | λx. e | e1 e2 | e1 , , e2.|A→B | AB∅ | Γ, x : A

x | () | λx. e | v1 , , v2

ѮF FYQSFTTJPOT e BSF DPOWFOUJPOBM FYDFQU GPS UIF NFSHF FYQSFTTJPO e1 , , e2 XIJDI EFTDSJCFT UIBU UXP FYQSFTTJPOT DBO CF NFSHFE CZ B NFSHF PQFSBUPS , , ѮF UZQFT A BSF UPQUZQFT GVODUJPO UZQFT BOE JOUFSTFDUJPO UZQFT 7BMVFT BSF NPTU TUBOEBSE FYDFQU GPS NFSHFT
v1 , , v2 FWFO UIPVHI UIFZ DBO TUFQ GVSUIFSϛϜϛ 4ĮěĭĲĩĢħĠ Ěħĝ 5ĲĩĢħĠ
4VCUZQJOH JT TIPXO JO 'JHVSF  ѮF SVMFT GPS BSSPX BOE JOUFSTFDUJPO UZQFT BSF TUBOEBSEѮF CJEJSFDUJPOBM UZQJOH JT TIPXO JO 'JHVSF  3VMF 5.īĠ*ħğ JT UIF JOUSPEVDUJPO UZQJOH
SVMF GPS UIF NFSHF PQFSBUPS e1 , , e2 IBT UIF UZQF A1  A2 JG e1 IBT UIF UZQF A1 BOE e2 IBTUIF UZQF A2  3VMF 5.īĠ*ħğ, JT UIF FMJNJOBUJPO SVMF e1 , , e2 IBT UIF UZQF A JG POF PG UIF #BDLHSPVOE
4VCUZQJOH

A≤B
4"īī

B  ≤ A

4"ħĝ,45Ĩĩ

A ≤ B A ≤ hQT

A → A ≤ B  → B 

4"ħĝ

Ak ≤ BA ≤ B

A  A ≤ B

A ≤ B

A ≤ B  B'JHVSF  %VOêFMET 4VCUZQJOH#JEJSFDUJPOBM 5ZQJOH

Γ'e:A
57Ěī

5.īĠ$),,5.īĠ*ħğ,Γ ' e , , e  ⇐ A

Γ ' e , , e  ⇒ A

Γ ' ek ⇐ A

x : A in Γ
Γ'Y⇒A5.īĠ*ħğΓ ' e  ⇒ A

Γ ' ek ⇒ A

5-ĚĦΓ, Y : A ' e ⇐ B

Γ ' e  ⇒ A

Γ ' e  , , e  ⇒ A  A5"ĩĩ

Γ ' e ⇒ A → B

Γ ' e ⇐ A

Γ ' e e ⇒ B

Γ ' λY. e ⇐ A → B
54Įě

5"ħħ

Γ'e⇐A

Γ'e⇒A

Γ'e:A⇒A

A≤B

Γ'e⇐B

'JHVSF  %VOêFMET 5ZQJOHCSBODI e1 PS e2 IBT UIF UZQF A  ѮF EFTJHO JT ëFYJCMF UP FODPEF NBOZ GFBUVSFT JODMVEJOH
GVODUJPO PWFSMPBEJOH BOE SFDPSE QSPKFDUJPO UIPVHI MFBEJOH UP OPOEFUFSNJOJTUJD JOGFSFODF
TJODF JU JT OPU TZOUBYEJSFDUFE'ĞĚĭĮīĞ &ħĜĨĝĢħĠ ѮF UZQJOH JT WFSZ QPXFSGVM BOE FOBCMFT JOGFSFODF GPS UIF BQQMJDBUJPO'PS FYBNQMF b?Qr JT UIF NFSHF PG b?QrAMi BOE b?Qr"QQH 8F TIPX UIF UZQJOH FYBNQMF GPS
UIF b?Qr R∅ ' b?QrAMi ⇒ AMi → ai`BM;∅ ' b?Qr ⇒ AMi → ai`BM;

5.īĠ*ħğ,∅ ' b?Qr 1 ⇒ ai`BM;∅ ' 1 ⇐ AMi

5"ĩĩ 5ZQF%JSFDUFE 0QFSBUJPOBM 4FNBOUJDTϛϜϜ &ĥĚěĨīĚĭĢĨħ 4ĞĦĚħĭĢĜĬ
%VOêFMET DBMDVMVT FNQMPZT B OPOEFUFSNJOJTUJD FMBCPSBUJPO TFNBOUJDT ѮF DBMDVMVT XJUIJOUFSTFDUJPO UZQFT DBO CF FMBCPSBUFE UP UIF DBMDVMVT XJUI QSPEVDU UZQFT *O UIF FMBCPSBUJPOUIF FYQMJDJU FMJNJOBUJPO PG QSPEVDU UZQFT XJMM CF JOTFSUFE BѫFS UIF UZQF DIFDLJOH /PUF UIBUUIFSF JT BMTP B PQFSBUJPOBM TFNBOUJDT UIPVHI JU TJNQMZ IFMQT DIFDL UIF DPSSFDUOFTT PG UIFFMBCPSBUJPO BOE EPFT OPU BDUVBMMZ NPEFM UIF DPNQVUBUJPO QSPDFTTϛϝ 5ĲĩĞ%ĢīĞĜĭĞĝ 0ĩĞīĚĭĢĨħĚĥ 4ĞĦĚħĭĢĜĬ*O DMBTTJDBM DBMDVMJ FH 4JNQMZ 5ZQFE -BNCEB $BMDVMJ UZQFT BSF VTVBMMZ FSBTFE JO UIF EZOBNJD TFNBOUJDT *O DPOUSBTU XJUI UZQFFSBTVSF TFNBOUJDT UZQFEFQFOEFOU BMTP LOPXO BT
UZQFQBTTJOH TFNBOUJDT NBLFT VTF PG UIF UZQFT JO UIF FWBMVBUJPO UP NBLF SVOUJNF EFDJTJPOT*O NPSF SFBMJTUJD QSPHSBNNJOH MBOHVBHFT XIFSF UZQFT BSF SFRVJSFE UP BTTJTU UIF FWBMVBUJPOUIF FMBCPSBUJPO TFNBOUJDT JT PѫFO BEPQUFE ѮBU JT UP TBZ MBOHVBHFT XJUI SVOUJNF EFDJTJPOTBSF FMBCPSBUFE UP BOPUIFS MBOHVBHF XJUIPVU UIFN " OPUBCMF FYBNQMF JT UZQF DMBTTFT XIJDIJT BO BQQSPBDI UP TVQQPSU QBSBNFUSJD PWFSMPBEJOH BOE IBT CFFO JODPSQPSBUFE BT UIF NBJOGFBUVSF JO MBOHVBHFT MJLF )BTLFMM ѮF NBJO JEFB JT UP USBOTMBUF B GVODUJPO UZQFE XJUI DMBTTJOUP B GVODUJPO XJUI B EJDUJPOBSZ XIJDI XJMM CF QBTTFE BU UIF SVOUJNF ѮJT JOTQJSFT NBOZEFTJHOT MJLF JNQMJDJUT JO 4DBMB <0MJWFJSB FU BM > BOE JOTUBODF BSHVNFOUT JO "HEB <%FWSJFTF
BOE 1JFTTFOT >
5ZQFEFQFOEFOU TFNBOUJDT TUJMM IBT JUT PXO BEWBOUBHFT PWFS UIF FMBCPSBUJPO TFNBOUJDTUIPVHI UIF MBUUFS JT VTVBMMZ DIPTFO JO B QSBDUJDBM TFOTF
r &MBCPSBUJPO TFNBOUJDT JT VTVBMMZ HJWFO JOEJSFDUMZ BOE DPNQMJDBUFT UIF SFBTPOJOH TJODF
XF OFFE UP TUVEZ CPUI UIF TFNBOUJDT PG TPVSDF BOE UBSHFU MBOHVBHFT 'VSUIFSNPSFUIF NFUBUIFPSZ PG DPIFSFODF JT RVJUF DIBMMFOHJOH TJODF UIF FRVJWBMFODF OFFET UP CFFTUBCMJTIFE
r ѮF TUBOEBSE EFUFSNJOJTN BOE TVCKFDUSFEVDUJPO DBO CF QSPWFE VTJOH EJSFDU TFNBOUJDT XIJMF UIPTF DBOOPU CF QSPWFO JO FMBCPSBUJPO TFNBOUJDT
0OF SFDFOU XPSL PG UZQFEFQFOEFOU TFNBOUJDT JT UZQFEEJSFDUFE PQFSBUJPOBM TFNBOUJDT
5%04 <)VBOH BOE 0MJWFJSB > *U JT êSTUMZ JOUSPEVDFE GPS DBMDVMJ XJUI JOUFSTFDUJPO UZQFTBOE B NFSHF PQFSBUPS *U FOBCMFT B OBUVSBM QSPPG PG EFUFSNJOJTN BOE TVCKFDUJPOSFEVDUJPO PG
UIF DBMDVMJ #BDLHSPVOEѮF NBJO JEFB PG 5%04 JT UIF VUJMJTBUJPO PG UZQF BOOPUBUJPOT 5ZQF BOOPUBUJPOT BSF EJTDBSEFE JO NBOZ DPOWFOUJPOBM MBOHVBHFT XJUI PQFSBUJPOBM TFNBOUJDT *U JOTUFBE XJMM CF VTFEJO UXP QMBDFT JO 5%04
r 5SJHHFS UIF $BTUJOH "OOPUBUJOH WBMVFT XJMM GPSDF UIFN UP CF DBTU JOUP UIF DPSSFTQPOEJOH
JUFNT BDDPSEJOH UP UIF UZQF QSPWJEFEr 5ZQFE 3FEVDUJPO ѮF DBTUJOH KVEHNFOU v )→A v " PSJHJOBMMZ DBMMFE UZQFE SFEVDUJPOBDDFQU POF JOQVU WBMVF v BOE POF JOQVU UZQF A UIFO DBTU v JOUP BOPUIFS WBMVF v " BDDPSEJOH UP UIF UZQF A 'PS FYBNQMF R--i`m2 , AMi XJMM CF FWBMVBUFE UP R

5%04 IBT BMTP CFFO TUVEJFE UP TVQQPSU HSBEVBM UZQJOH BOE BTTJTU JUT SVOUJNF DIFDLJOH <:F
FU BM >Ϝ "ĩĩĥĢĜĚĭĢįĞ 4ĮěĭĲĩĢħĠ*O UIJT TFDUJPO XF TUBSU XJUI BO JOUSPEVDUJPO UP DMBTTJDBM TVCUZQJOH BMHPSJUINT GPS JOUFSTFDUJPO UZQFT EJTDVTT TPNF EFTJHO PQUJPOT UP EFBM XJUI UIF JOGFSFODF PG BQQMJDBUJPOT BOE UIFOQSFTFOU BQQMJDBUJWF TVCUZQJOH "QQMJDBUJWF TVCUZQJOH JT BCMF UP DPNQVUF UIF PVUQVU UZQF PG
BQQMJDBUJPOT JO UIF QSFTFODF PG PWFSMPBEJOH BOE OFTUFE DPNQPTJUJPO ѮFO XF NBLF BO BOBM
PHZ PG SFDPSE QSPKFDUJPOT ѮVT JO UIF DPOUFYU PG DBMDVMJ XJUI JOUFSTFDUJPO UZQFT BQQMJDBUJWFTVCUZQJOH QSPWJEFT B VOJêFE TPMVUJPO UP JOGFS UZQFT GPS BQQMJDBUJPOT BOE SFDPSE QSPKFDUJPOT
5XP WFSTJPOT PG TVCUZQJOH PG JOUFSTFDUJPO UZQFT BSF QSFTFOUFE POF JT UIF TVCUZQJOH XJUIPVU
EJTUSJCVUJWJUZ BOE POF JT UIF #$% TVCUZQJOH XJUI EJTUSJCVUJWJUZ JODMVEFE ѮFO XF JOUFSQSFUFBDI SVMF JO UFSNT PG PWFSMPBEJOH BOE QSPKFDUJPO BOE EFTDSJCF TFWFSBM DIBMMFOHFT PG EFBM
JOH XJUI UIF JOGFSFODF PG UIF BQQMJDBUJPO UZQFT BOE QSPKFDUJPO UZQFT *O UIF GPMMPXJOH XF
EFWFMPQ PVS UXP NBJO NFUIPET BQQMJDBUJPO NPEF BOE BQQMJDBUJWF TVCUZQJOH "QQMJDBUJPONPEF DBO CF USFBUFE BT B TUBDLCBTFE SFTPMVUJPO PG BQQMJDBUJWF TVCUZQJOH BOE DPSSFTQPOET UPUIF TVCUZQJOH XJUIPVU EJTUSJCVUJWJUZ *OTUFBE BQQMJDBUJWF TVCUZQJOH JOTUBOUMZ DPNQVUFT UIF
BQQMJDBUJPO UZQFT XJUIPVU UIF OFDFTTJUZ PG DPMMFDUJOH BMM UIF BSHVNFOU UZQFT BOE DPSSFTQPOETUP UIF EJTUSJCVUJWF TVCUZQJOH 8F FYBNJOF UIF NFUBUIFPSZ PG BQQMJDBUJWF TVCUZQJOH JO UIF
MBTUϜϚ 5ĲĩĞĬ
8F TUBSU XJUI UIF TZOUBY PG UZQFT
5ZQFT
0SEJOBSZ 5ZQFT

A, B ::= AMi | hQT | A → B | A  B

Ao , B o ::= AMi | hQT | A → B o

A BOE B BSF NFUBWBSJBCMFT XIJDI SBOHF PWFS UZQFT AMi BOE hQT BSF CBTF UZQFT BOE hQT JTUIF TVQFSUZQF PG BMM UZQFT $PNQPVOE UZQFT BSF GVODUJPO UZQFT A → B JOUFSTFDUJPO UZQFT

A  B 0SEJOBSZ UZQFT <%BWJFT BOE 1GFOOJOH  )VBOH FU BM > BSF FTTFOUJBMMZ UZQFTXJUIPVU JOUFSTFDUJPO UZQFT FYDFQU GPS GVODUJPOT XIFSF JOUFSTFDUJPO UZQFT DBO BQQFBS JO BSHVNFOU UZQFT "T XF XJMM TFF MBUFS PSEJOBSZ UZQFT BSF IFMQGVM JO UIF EFêOJUJPO PG BMHPSJUINJD
TVCUZQJOH "QQMJDBUJWF 4VCUZQJOHϜϛ 4ĮěĭĲĩĢħĠ Ěħĝ #$% 4ĮěĭĲĩĢħĠ
4VCUZQJOH SFMBUJPOT GPS JOUFSTFDUJPO UZQFT DBO WBSZ JO XIFUIFS EJTUSJCVUJWJUZ SVMFT BSF JODMVEFEPS OPU 'PS DBMDVMJ XJUI JOUFSTFDUJPO UZQFT B DPNNPO SVMF BMMPXT UIF JOUFSTFDUJPO PG BSSPXUZQFT UP EJTUSJCVUF PWFS BSSPXT 8F QSFTFOU UXP WFSTJPOT PG TVCUZQJOH BOE UIFO EFSJWF PVS
BQQSPBDI SFTQFDUJWFMZϜϛϚ 4ĮěĭĲĩĢħĠ
4VCUZQJOH

A≤B
4"īī

4*ħĭ

45Ĩĩ

AMi ≤ AMiA ≤ hQT

C≤A

4"ħĝ

B≤D

A ≤ B

A ≤ B  B

A→B≤C→D

4"ħĝ-4"ħĝ3

AB ≤ CAB ≤ CA≤CA ≤ BB≤C'JHVSF  4VCUZQJOH*O 'JHVSF  XF QSFTFOU UIF SVMFT GPS TVCUZQJOH 3VMFT 4*ħĭ BOE 45Ĩĩ EFTDSJCFT CBTFUZQFT AMi BOE hQT AMi JT UIF TVCUZQF PG JUTFMG BOE hQT JT UIF TVQFSUZQF PG BOZ UZQF 'PS
GVODUJPOT SVMF 4"īī TBZT UIBU A → B JT UIF TVCUZQF PG C → D JG A JT UIF TVQFSUZQF PG C

BOE B JT UIF TVCUZQF PG D 0O UIF PUIFS IBOE UIF TVCUZQJOH SFMBUJPO PG UIFJS JOQVU UZQFT JT
DPOUSBWBSJBOU BOE UIF TVCUZQJOH SFMBUJPO PG UIFJS PVUQVU UZQFT JT DPWBSJBOU
3VMFT 4"ħĝ 4"ħĝ- BOE 4"ħĝ3 BSF VTFE GPS JOUFSTFDUJPOT UZQF A JT UIF TVCUZQF PG
UIF JOUFSTFDUJPO UZQF B1  B2 JG JU JT UIF TVCUZQF PG CPUI CSBODIFT B1 BOE B2  ѮF JOUFSTFDUJPO UZQF A  B JT UIF TVCUZQF PG C JG UIFSF FYJTUT POF CSBODI UIBU JT UIF TVCUZQF PG C

3ĞĦĚīĤ 8F DBO QSPWF UIBU UIF TVCUZQJOH SFMBUJPO JT SFëFYJWF BOE USBOTJUJWF ѮVT UIF GPMMPXJOH UXP SVMFT BSF EFSJWBCMF GSPN UIF SVMFT JO 'JHVSF 43Ğğĥ



A≤A

45īĚħĬ

A≤B

B≤C

A≤C

 4VCUZQJOH BOE #$% 4VCUZQJOH
A " A # A

4QMJUUBCMF 5ZQFT
4ĩ"īī

4ĩ"ħĝ

A " AB # B

B " B # BA → B " A → B # A → B
4VCUZQJOH

A <: B
4Įě*ħĭ

4Įě5Ĩĩ

AMi <: AMi

A <: hQT

4Įě"ħĝ

B " B # BA <: BA <: B

4Įě"īī

C <: AB <: DoA → B <: C → Do
4Įě"ħĝ-4Įě"ħĝ3A  B <: C o

A  B <: C o

A <: C o

A <: BB <: C o'JHVSF  4QMJUUBCMF 5ZQFT BOE #$% 4VCUZQJOHϜϛϛ #$% 4ĮěĭĲĩĢħĠ
0OF XFMMLOPXO TVCUZQJOH SFMBUJPO XJUI TVDI B EJTUSJCVUJWJUZ SVMF JT #$% TVCUZQJOH <#BSFO
ESFHU FU BM >
4%ĢĬĭī

(A → B)  (A → C) ≤ A → (B  C)

3VMF 4%ĢĬĭī TBZT JOUFSTFDUJPO UZQFT DBO EJTUSJCVUF PWFS GVODUJPO UZQFT )VBOH FU BM
<> QSPWJEF B TPVOE BOE DPNQMFUF BMHPSJUIN GPS #$% TVCUZQJOH CZ FMJNJOBUJOH UIF USBOTJUJWJUZ SVMF BOE FNQMPZJOH UIF OPUJPOT PG PSEJOBSZ UZQFT BOE TQMJUUBCMF UZQFT 4QMJUUBCMF UZQFTEFTDSJCF UIBU UZQFT DBO CF TQMJU JOUP UXP TJNQMFS UZQFT BOE PSEJOBSZ UZQFT BSF UIPTF XIJDIDBOOPU CF TQMJU8F QSFTFOU TQMJUUBCMF UZQFT BOE UIF TVCUZQJOH SFMBUJPO JO 'JHVSF  5P EJTUJOHVJTI CFUXFFO UIF BCPWF TVCUZQJOH SFMBUJPO XF VTF <: JOTUFBE PG ≤ IFSF  3VMF 4Įě"ħĝ JT UIF NPTUJOUFSFTUJOH SVMF BT JU DBQUVSFT UIF EJTUSJCVUJWJUZ PG JOUFSTFDUJPO UZQFT PWFS GVODUJPO UZQFT ѮJT
SVMF TQMJUT UIF UZQF B JOUP UXP UZQFT B1 BOE B2 BOE QSPDFFET CZ UFTUJOH XIFUIFS A JT B TVCUZQF PG CPUI B1 BOE B2 BOE TBZT A JT UIF TVCUZQF PG B JG A BSF TVCUZQFT PG JUT TQMJUT A1 BOE
A2  3VMFT 4Įě"ħĝ- BOE 4Įě"ħĝ3 EFTDSJCF UIBU JOUFSTFDUJPO UZQF A  B JT UIF TVCUZQF
PG PSEJOBSZ UZQF C JG POF PG UIFN JT UIF TVCUZQF PG JU "QQMJDBUJWF 4VCUZQJOH.ĞĭĚĭġĞĨīĲ ѮF BMHPSJUINJD #$% TVCUZQJOH IBT UIF GPMMPXJOH JOUFSFTUJOH QSPQFSUJFT-FNNB  (FOFSBMJTBUJPO PG TVCUZQJOH t *G B <: D BOE C <: A UIFO A → B <: C → Dt *G A <: C UIFO A  B <: Ct *G B <: C UIFO A  B <: C
-FNNB  3FëFYJWJUZ PG #$% 4VCUZQJOH  A <: A
-FNNB  5SBOTJUJWJUZ PG #$% 4VCUZQJOH  *G A <: B BOE B <: C UIFO A <: CϜϜ *ħĭĞīĬĞĜĭĢĨħ 4ĮěĭĲĩĢħĠ Ěħĝ 0įĞīĥĨĚĝĢħĠ*O UIJT TFDUJPO XF XJMM TUVEZ UIF DPOOFDUJPO CFUXFFO JOUFSTFDUJPO TVCUZQJOH BOE GVODUJPOPWFSMPBEJOH JO EFUBJM 4JODF UIF UXP WBSJBOUT PG TVCUZQJOH BSF TIPXO BCPWF XF QSPWJEF UXPJOUFSQSFUBUJPOT PG PWFSMPBEJOH 0OF JT UIF PWFSMPBEJOH SFTPMVUJPO XJUI BMM UIF BSHVNFOUTHJWFO XIJDI êUT JOUP PVS GBNJMJBS LOPXMFEHF PG PWFSMPBEJOH "OPUIFS JOUFSQSFUBUJPO JT SBUIFS
TJNQMF BOE OPWFM DVSSJFE PWFSMPBEJOHϜϜϚ *ħĭĞīĩīĞĭĚĭĢĨħ Ĩğ 4ĮěĭĲĩĢħĠ 3ĮĥĞĬ
*OUFSTFDUJPO UZQFT BSF OBUVSBMMZ VTFGVM GPS SFQSFTFOUJOH UZQFT PG PWFSMPBEFE GVODUJPOT ѮF
UZQF PG PWFSMPBEFE GVODUJPOT JT UIF BOE  DPNCJOBUJPO PG UZQFT GSPN FBDI JOTUBODF 'PS
FYBNQMF JG b?Qr IBT UXP JOTUBODFT b?QrAMi BOE b?Qr"QQH ѮFO UIF UZQF PG b?Qr JT UAMi
→ ai`BM;V  U"QQH → ai`BM;V"T XF NFOUJPOFE BCPWF TVCUZQJOH EFTDSJCFT UIF SFMBUJPO CFUXFFO UZQFT ѮF TVCUZQJOH

PG JOUFSTFDUJPO UZQFT JT VTFGVM GPS UFMMJOH VT JOGPSNBUJPO BCPVU PWFSMPBEJOH /PUF UIBU JO UIFSFMBUJPO A ≤ B UIF MFѫ TJEF A QMBZT UIF SPMF PG PWFSMPBEFE GVODUJPOT BOE UIF SJHIU TJEF B
QMBZT UIF SPMF PG BSHVNFOUT BOE SFTVMUT UBLF JU GPS HSBOUFE GPS OPX 

r 3VMF 4"īī UFMMT UIBU GPS B GVODUJPO IBWJOH UIF UZQF A → B XJUI BO BSHVNFOU UZQF C
BOE B SFTVMU UZQF D HJWFO XF DIFDL UIFJS DPSSFDUOFTT WJB UIF TVCUZQJOH SFMBUJPOT

r 3VMFT 4"ħĝ- BOE 4"ħĝ3 UFMMT UIBU C DBO CF EFSJWFE PVU JG TPNF PG A  B DBOEFSJWF PVU UIF C ѮJT JT BMTP IFMQGVM GPS UFMMJOH VT XIFUIFS POF CSBODI CFMPOHT UP UIFPWFSMPBEJOH JOTUBODFT 'PS FYBNQMF XF DBO LOPX UIBU b?QrAMi JT POF CSBODI PG b?Qr
XJUI UIF TVCUZQJOH TUBUFNFOU UAMi → ai`BM;V  U"QQH → ai`BM;V I, AMi →ai`BM; *OUFSTFDUJPO 4VCUZQJOH BOE 0WFSMPBEJOH
r 3VMF 4%ĢĬĭī JT UIF JOUFSFTUJOH SVMF "ѫFS UIJT SVMF JT BEEFE XF DBO LOPX (A →B)  (A → C) JT JTPNPSQIJD XJUI A → (B  C) 3FëFDUJOH JO WBMVFT UFSNT

λx. e1 , , λx. e2 TIPVME CF iJTPNPSQIJDu XJUI λx. (e1 , , e2 ) JO TPNF TFOTF ѮJT XJMM
JOUSPEVDF UIF OFX OPUJPO XF OBNF JU ĕSTUDMBTT DVSSJFE PWFSMPBEFE GVODUJPOϜϜϛ *ħĭĞīĬĞĜĭĢĨħ 4ĮěĭĲĩĢħĠ 1ĚīĭĢĚĥĥĲ
1SFWJPVTMZ XF BTTVNFE UIBU UIF TVCUZQJOH SFMBUJPO CVJMET PO UIF GBDU UIBU UIF SFTVMU UZQF GPS
BQQMJDBUJPOT JT LOPXO )PXFWFS UIJT JT OPU UIF DBTF JO PWFSMPBEFE BQQMJDBUJPOT XIFSF POMZUIF BSHVNFOU UZQFT BSF LOPXO #BTJDBMMZ XF USZ UP TPMWF UIF QSPCMFN JO UIF GPMMPXJOH GPSNXIFSF XF JOGFS UIF UZQF \ HJWFO UIF BSHVNFOU UZQF AMi(AMi → ai`BM;)  ("QQH → ai`BM;) <: AMi →?
8F UIFO JOUSPEVDF UIF SFMBUJPO A <: P $ O XIFSF P TUBOET GPS QBSUJBM UZQFT BOE O TUBOETGPS PVUQVU UZQFT ѮF PSJHJOBM TVCUZQJOH DBO CF USFBUFE BT B TQFDJBM DBTF XIFO A <: B $ ∅ ѮF GPSNBM EFêOJUJPO PG P BOE O JT TIPXO BT GPMMPXT
1BSUJBM 5ZQFT

P ::= A | A→

0VUQVU 5ZQFT

O ::= A | ∅ѮFO UIF DPSSFTQPOEJOH SVMFT BSF TQFDJBMMZ BEBQUFE GPS QBSUJBM UZQFT
4"īī1Ěī

4"ħĝ-1Ěī

C <: AA → B <: C→ $ B

A <: C→ $ D

A  B <: C→ $ D

4"ħĝ31Ěī

B <: C→ $ D

A  B <: C→ $ D

8JUI OFX SVMFT XF DBO DPODMVEF TPNF JOUFSFTUJOH DBTFT 'PS FYBNQMF UIF SFTVMU UZQF PG
b?QrAMi--b?Qr"QQH R JT ai`BM;

Int <: Int
Int → String <: Int→ $ String

4"īī1Ěī

(Int → String)  (Bool → String) <: Int→ $ String

4"ħĝ-1Ěī "QQMJDBUJWF 4VCUZQJOHѮF DIBMMFOHJOH QBSU JT IPX UP EFBM XJUI UIF DBTF 7--; R XIFSF 7 IBT UIF UZQF AMi → AMi→ AMi BOE ; IBT UIF UZQF AMi → "QQH → "QQH  "DDPSEJOH UP PVS SVMFT TIPXO UIFSF BSF

UXP QPTTJCMF SFTVMUT AMi → AMi BOE "QQH → "QQH #PUI BSF OPU JEFBM 8F UIFO DBO IBWFUXP DIPJDFT IFSF

r 3FKFDU CFDBVTF JU DBOOPU NBLF B DIPJDF ѮFO EFBMJOH XJUI UIF DBTF 7--; R i`m2
XIFSF ; DBO CF TFMFDUFE BDDPSEJOH UP UIF UXP BSHVNFOUT R BOE i`m2 JT TUJMM B QSPCMFN
r "DDFQU BOE EFSJWF UIF SFTVMU UAMi → AMiV  U"QQH → "QQHV XIJDI DPSSFTQPOET UPUIF EJTUSJCVUJWJUZ SVMF JO TVCUZQJOH

8F XJMM EFWFMPQ UXP DIPJDFT JO TFDUJPO  BOE Ϝϝ $ġĚĥĥĞħĠĞĬ Ĩğ "ĩĩĥĢĜĚĭĢĨħ 5ĲĩĢħĠ*O B USBEJUJPOBM UZQF TZTUFN XJUI CJEJSFDUJPOBM UZQJOH XF FYQFDU UIBU PVS UZQJOH SVMF GPS
BQQMJDBUJPOT JT JO UIF GPMMPXJOH GPSNΓ ' e1 ⇒ A → B

Γ ' e2 ⇐ A

Γ ' e1 e2 ⇒ B

5"ĩĩ

3VMF 5"ĩĩ EPFT UXP UIJOHT ѮF êSTU JT UP DIFDL XIFUIFS e1 e2 JT XFMMUZQFE XIJDI SFRVJSFT
e1 UP JOGFS UIF BSSPX UZQF BOE e2 DBO CF DIFDLFE CZ UIF JOQVU GSPN UIF BSSPX UZQF 4FDPOEJU JOGFST UIF UZQF GPS UIF BQQMJDBUJPO UFSN FH B JO UIJT DBTF ѮF TUPSZ CFDPNFT EJĒFSFOU XIFO XF JOUSPEVDF JOUFSTFDUJPO UZQFT XIJDI NBZ DBVTF UIFUZQF PG e1 UP CF BO JOUFSTFDUJPO UZQF XIJDI JT
Γ ' e1 ⇒ A  B

Γ ' e2 ⇐ ?

Γ ' e1 e2 ⇒ ?

5"ĩĩ

*O UIJT TJUVBUJPO XF DBOOPU TJNQMZ FYUSBDU UIF JOQVU UZQF GSPN A  B UP DIFDL e2 BOE DBOOPUEFSJWF UIF SFTVMU UZQF GPS UIF BQQMJDBUJPO UFSN.FSHF PQFSBUPS IBT IJHIFS QSFDFEFODF UIBO BQQMJDBUJPO "QQMJDBUJPO .PEF

ϜϞ "ĩĩĥĢĜĚĭĢĨħ .ĨĝĞ5P BEESFTT UIJT QSPCMFN XF CPSSPX UIF JEFB PG BO BQQMJDBUJPO NPEF <9JF BOE 0MJWFJSB >
"U êSTU UIJT JEFB MPPLT QSPNJTJOH CVU B NPSF DBSFGVM MPPL SFWFBMT TPNF JTTVFT

5ġĞ "ĩĩĥĢĜĚĭĢĨħ .ĨĝĞ 9JF BOE 0MJWFJSB <> TVHHFTUFE BO BMUFSOBUJWF BQQSPBDI UPCJEJSFDUJPOBM UZQF DIFDLJOH UIBU FNQMPZT B HFOFSBMJTBUJPO PG UIF JOGFSFODF NPEF ѮF LFZJEFB JT UP VTF UIF UZQF GSPN BSHVNFOUT UP JOGFS UIF GVODUJPO UZQF *O UIFJS XPSL UIF JOGFS
FODF GPDVTFT PO UIF IJHIFSSBOL QPMZNPSQIJD GVODUJPO ѮF BQQMJDBUJPO NPEF HFOFSBMJTFTUIF TZOUIFTJT NPEF BOE Γ ' e ⇒ A JT TZOUBDUJD TVHBS XIFO UIF BSHVNFOU TUBDL Ψ JT FNQUZ
8JUI UIF BQQMJDBUJPO NPEF UIF SVMF GPS BQQMJDBUJPOT JTΓ ' e2 ⇒ A

Γ ! Ψ, A ' e1 ⇒ A → B

Γ ! Ψ ' e1 e2 ⇒ B

5"ĩĩѮF NPUJWBUJOH FYBNQMF GPS EFNPOTUSBUJOH UIF BEWBOUBHFT PG UIF BQQMJDBUJPO NPEF JT UP UZQF
DIFDL UIF UFSN (λx. x) 1 *O B USBEJUJPOBM TZTUFN XJUI CJEJSFDUJPOBM UZQJOH (λx. x) SFRVJSFTBO FYQMJDJU BOOPUBUJPO TJODF UIF VOUZQFE MBNCEB BCTUSBDU TIPVME CF JO DIFDL NPEF 6OEFSUIF BQQMJDBUJPO NPEF XF DBO HJWF UIF UZQJOH EFSJWBUJPOT GPS UIJT UFSN
. ' R ⇒ AMi. ! AMi ' λx. x ⇒ AMi → AMi. ' (λx. x) R ⇒ AMi

5"ĩĩ

)FSF XF DBO NBLF BO BOBMPHZ BOE VTF UIJT UFDIOJRVF UP JOGFS UIF GVODUJPO UZQF XJUI JOUFSTFDUJPO UZQFT 4JODF JOUFSTFDUJPO UZQFT A  B QMBZ UIF SPMF PG êOJUF QPMZNPSQIJD UZQF 'PS
JOTUBODF b?Qr k TIPVME TFMFDU CSBODI b?QrAMi BOE IBT UIF UZQF ai`BM;
. ' R ⇒ AMi. ! AMi ' b?QrAMi--b?Qr"QQH ⇒ AMi → ai`BM;. ' b?QrAMi--b?Qr"QQH R ⇒ ai`BM;

5"ĩĩ

8F QSFTFOU B EFTJHO PG B TUBDLCBTFE BQQSPBDI JO 'JHVSF  3VMF "Ĭ3Ğğĥ JT UIF SFëFYJWJUZ
SVMF UZQF A SFUVSOT UIF UZQF JUTFMG XIFO UIF BSHVNFOU JT FNQUZ 3VMF "Ĭ"īī LFFQT DPOTVNJOH UIF BSHVNFOUT JO UIF TUBDL CZ FMJNJOBUJOH UIF JOQVU UZQFT PG BSSPX UZQFT 3VMFT "Ĭ"ħĝBOE "Ĭ"ħĝ3 EFSJWF UIF SFTVMU D GSPN FJUIFS UIF MFѫ PS SJHIU CSBODIFT /PUF UIBU XF IBWFB TQFDJBM KVEHNFOU Ψ ' A <: B JO UIF QSFNJTF BT OFHBUJPO XIJDI JT UIF CJOBSZ WFSTJPO PG

Ψ ' A <: B BOE UIF OFHBUJPO Ψ ' A TBZT BOZ CSBODIFT JO A DBOOPU BDDFQU UIF BSHVNFOUT "QQMJDBUJWF 4VCUZQJOH"QQMJDBUJWF 4VCUZQJOH

Ψ ' A <: B"43Ğğĥ

· ' A <: A"4"īī

C <: AΨ ' B <: D

Ψ, C ' A → B <: C → D"4"ħĝ3

Ψ, C ' B <: D"4"ħĝ-Ψ, C ' A <: D

¬ Ψ, C ' B

Ψ, C ' A  B <: D

¬ Ψ, C ' A

Ψ, C ' A  B <: D

'JHVSF  "QQMJDBUJWF 4VCUZQJOH 4UBDLJO UIF TUBDL #Z UIJT EFTJHO XF DBO BDDFQU 7--; R i`m2 BOE SFKFDU 7--; R 8F TIPX UIFFYBNQMF CFMPX"QQH <: "QQH
AMi <: AMi· ' "QQH <: "QQH

"QQH ' "QQH → "QQH <: "QQH

"QQH, AMi ' (AMi → "QQH → "QQH) <: "QQH

"43Ğğĥ
"4"īī
"4"īī

"QQH, AMi ' (AMi → AMi → AMi)  (AMi → "QQH → "QQH) <: "QQH

"4"ħĝ3

ѮF BDDPNQBOZJOH UZQJOH GPS UIF BQQMJDBUJPO NPEF JT TIPXO JO 'JHVSF  3VMF 5Ĳ7Ěī
SFTPMWFT UIF TUBDL CZ DPNQVUJOH UIF SFTVMU GPS WBSJBCMFT 3VMF 5Ĳ-ĚĦ JT UIF TUBOEBSE SVMF GPS
MBNCEB BCTUSBDUJPOT 3VMF 5Ĳ-ĚĦ4 SFTPMWFT UIF TUBDL CZ DIFDLJOH UIF UZQFT BOE UZQFT JO
UIF TUBDL 3VMF 5Ĳ"ĩĩ JT UIF POMZ SVMF UP DPMMFDU UIF UZQFT PG BSHVNFOUT BOE QVTI UIFN UP
UIF TUBDL Ψ 3VMF 5Ĳ"ħħ SFTPMWFT UIF TUBDL BOE EFSJWFT UIF SFTVMU 3VMF 5Ĳ.īĠ JT UIF TUBOEBSE SVMF 3VMF 5Ĳ.īĠ JOGFST UIF UZQF XIJDI NBZ DPNF GSPN FJUIFS MFѫ PS SJHIU CSBODIFTBDDPSEJOH UP UIF TUBDL HJWFO
$ġĚĥĥĞħĠĞĬ Ģħ %ĲħĚĦĢĜ 4ĞĦĚħĭĢĜĬ ѮF SFBTPO UIBU UIF BQQMJDBUJPO NPEF IBT OPU CFFOBEPQUFE JO UIF DBMDVMJ JT UIBU JU JT DIBMMFOHJOH UP EFTJHO UIF DPSSFTQPOEJOH EZOBNJD TFNBOUJDT*O UIF TUBUJDT UIF JEFB JT UP DPMMFDU BMM UIF UZQFT PG BSHVNFOUT BOE UIFO NBLF UIF TFMFDUJPOGSPN PVUTJEF UP JOTJEF 4VQQPTF f BOE g BSF GVODUJPOT XJUI UIF GPMMPXJOH UZQFT
7 : AMi → AMi → AMi; : AMi → "QQH → "QQH

5P JOGFS UIF UZQF 7--; R i`m2 XF XJMM EP UISFF TUFQT
r 'JSTU XF FODPVOUFS i`m2 BOE QVTI JUT UZQF "QQH JOUP UIF TUBDL "QQMJDBUJWF 4VCUZQJOH"QQMJDBUJWF 5ZQJOH

Γ!Ψ'e⇔A
5Ĳ7Ěī

5Ĳ-Ģĭ

x:A∈T

Γ ! · ' J ⇒ AMi

5Ĳ-ĚĦ

Γ, Y : A ! · ' e ⇒ B

Ψ ' A <: B

Γ!Ψ'Y⇒A

5Ĳ-ĚĦ4

Γ, Y : A ! · ' e ⇒ B

Γ ! · ' λY. e : A → B ⇒ A → B

Ψ, C ' A → B <: D

Γ ! Ψ, C ' λY. e : A → B ⇒ D

5Ĳ"ĩĩ

Γ ! · ' e ⇒ A

Γ ! Ψ, A ' e ⇒ A → B

Γ ! Ψ ' e e ⇒ B

5Ĳ"ħħ

Γ!·'e⇒C

C <: AΓ!Ψ'e:A⇒B

5Ĳ.īĠ4-

Γ ! Ψ, A ' e ⇒ C

Ψ ' A <: B

Γ ! · ' e ⇒ B

Γ ! Ψ, A ' e1, , e2 ⇒ C

5Ĳ.īĠ

Γ ! · ' e ⇒ A

Γ ! · ' e ⇒ B

Γ ! · ' e1, , e2 ⇒ A  B

5Ĳ.īĠ43

Γ ! Ψ, A ' e ⇒ C

Γ ! · ' e ⇒ B

Γ ! Ψ, A ' e1, , e2 ⇒ C'JHVSF  "QQMJDBUJWF 5ZQJOH

r /FYU XF BOBMZTF 1 BOE QVTI JUT UZQF AMi JOUP UIF TUBDL
r -BTU VTJOH UIF DPOUFOUT PG UIF TUBDL XF JOGFS UIF UZQF PG 7--; JT AMi → "QQH → "QQHѮF PSEFS PG UZQF BOBMZTJT JT SFWFSTFE GSPN UIF PQFSBUJPOBM TFNBOUJDT CBTFE PO UIF DBMMCZWBMVF TUSBUFHZ *O EZOBNJD TFNBOUJDT PG UIF λDBMDVMVT 7-- ; R TIPVME CF FWBMVBUFE êSTU UP
B WBMVF BOE XF LOPX OPUIJOH BCPVU UIF TFDPOE BSHVNFOUϜϟ "ĩĩĥĢĜĚĭĢįĞ 4ĮěĭĲĩĢħĠ
"QQMJDBUJWF TVCUZQJOH JT BOPUIFS BQQSPBDI UP JOGFS UIF UZQFT PG BQQMJDBUJPOT BOE QSPKFDUJPOTXIJDI JT EJĒFSFOU GSPN BQQMJDBUJPO NPEF JO UISFF XBZTr "QQMJDBUJWF TVCUZQJOH DPSSFTQPOET UP UIF TVCUZQJOH SFMBUJPO XJUI EJTUSJCVUJWJUZ XIJMFUIF BQQMJDBUJPO NPEF EPFT OPU TVQQPSU EJTUSJCVUJWJUZ
r "QQMJDBUJWF TVCUZQJOH SFTPMWFT UIF BSHVNFOU JOTUBOUMZ BOE POFCZPOF XIJMF UIF MBUUFSSFTPMWFT UIF BSHVNFOU TUBDL BѫFS DPMMFDUJOH BMM UIF BSHVNFOUT "QQMJDBUJWF 4VCUZQJOH

A1 → A2 # B = A2
A1 → A2 # B = .

A1  A2 # S = (A1 # S) ! (A2 # S)
A#S =.

when B <: A1when ¬(B <: A1 )otherwise





'JHVSF  "QQMJDBUJWF 4VCUZQJOHr ѮF EFTJHO PG PQFSBUJPOBM TFNBOUJDT PG BQQMJDBUJWF TVCUZQJOH JT SFMBUJWFMZ FBTJFS XIJMFUIF MBUUFS JT DIBMMFOHJOH"QQMJDBUJWF TVCUZQJOH VUJMJTFT UIF OPUJPO PG TFMFDUPST UP êOE UIF DPSSFDU PVUQVU UZQF GSPN
BQQMJDBCMF UZQFT 8F DPOTJEFS BQQMJDBCMF UZQFT UP CF GVODUJPO PS SFDPSE UZQFT ѮJT SFMBUJPOFOBCMFT UIF UZQF TZTUFN UP JOGFS UIF UZQF PG BQQMJDBUJPOT BOE SFDPSE QSPKFDUJPOT ѮF UZQJOH
TUJMM BEPQUT CJEJSFDUJPOBM UZQJOH BOE VOMJLF UIF USBEJUJPOBM SVMFT GPS BQQMJDBUJPOT BOE QSPKFDUJPOT XF BMTP JOGFS UIF BSHVNFOU UZQFT UP IFMQ UIF JOGFSFODF PG BQQMJDBUJPO UZQF "T XF
DBO TFF CFMPX BQQMJDBUJWF TVCUZQJOH JT VTFE JO UIF SVMF 5"ĩĩ BOE IFMQ DPNQVUF UIF SFTVMUPG BQQMJDBUJPOT5"ĩĩΓ ' e ⇒ A

Γ ' e ⇒ B

A#B=C

Γ ' e e ⇒ C
8F NPEFM UIF UZQFT PG BSHVNFOUT BT TFMFDUPS UZQFT BOE UIF PVUQVUT BT CFJOH FJUIFS B UZQF PSOPUIJOH EFOPUJOH UIF GBJMVSF UP êOE B TVJUBCMF PVUQVU UZQF 
4FMFDUPS 5ZQFT

S ::= A0VUQVUTO ::= . | A

ѮF EFêOJUJPO PG BQQMJDBUJWF TVCUZQJOH JT HJWFO JO 'JHVSF  *U IBT UIF GPSN A # S = C

BOE JU SFBET BT UIF UZQF A DBO CF TFMFDUFE CZ UIF TFMFDUPS UZQF S BOE EFSJWF UIF SFTVMU UZQF C
4FMFDUPS UZQFT BSF VTFE BT UIF TFDPOE QBSBNFUFS BOE QSPQBHBUF UISPVHI UIF TVCUZQJOHDIFDLT VOUJM XF SFBDI BSSPX PS SFDPSE UZQFT 'PS BSSPX UZQFT JO SVMFT   XF DIFDLUIF DPOUSBWBSJBOU TVCUZQJOH CFUXFFO JOQVU UZQF A1 BOE BSHVNFOU B *G TVDDFTTGVM UIF PVUQVU UZQF A2 JT SFUVSOFE PUIFSXJTF XF GBJM 'PS UIF DBTF PG UIF JOUFSTFDUJPO UZQFT A1  A2
 XF JOUSPEVDF B DPNQPTJUJPO PQFSBUPS ! UP DPNCJOF UXP SFTVMUT XIJDI BSF EFSJWFE GSPN
BQQMZJOH A1 BOE A2 XJUI UIF TBNF TFMFDUPS UZQF B 3VMF  DPWFST B OVNCFS PG NJTTJOH

 "QQMJDBUJWF 4VCUZQJOHDBTFT TVDI BT AMi # S XIJDI XJMM BMM GBJM 'PS TJNQMJDJUZ PG QSFTFOUBUJPO XF XSJUF UIPTF
SVMFT BT B TJOHMF SVMF  

ѮF DPNQPTJUJPO PQFSBUPS ! BDDFQUT PVUQVU SFTVMUT BOE SFUVSOT B OFX PVUQVU SFTVMU ѮF
JTPMBUJPO PG UIF DPNQPTJUJPO PQFSBUPS HJWFT VT UIF BCJMJUZ UP NPEFM EJĒFSFOU GPSNT PG BQQMJDBUJWF TVCUZQJOH 8F QSFTFOU UXP EFTJHO PQUJPOT CFMPX/ĞĬĭĞĝ $ĨĦĩĨĬĢĭĢĨħ 4ĞĦĚħĭĢĜĬ *ĦĩĥĞĦĞħĭĚĭĢĨħ 'PS TZTUFNT XJUI #$% TVCUZQJOHXIJDI JODMVEFT EJTUSJCVUJWJUZ SVMFT XF VTF UIF DPNCJOBUPS JNQMFNFOUJOH UIF OFTUFE DPNQPTJUJPO TFNBOUJDT

A1 ! A2 = A1  A2



A1 ! .

= A1

. ! A2 = A2



.!.



=.

*G UXP PVUQVUT BSF CPUI UZQFT XF SFUVSO UIFJS JOUFSTFDUJPO UZQFT A1  A2 JO   ѮJT SVMF
NPEFMT UIF CFIBWJPVS PG OFTUFE DPNQPTJUJPO DPNCJOJOH UXP SFTVMUT *O  BOE  JG XF
IBWF BU MFBTU POF UZQF XF KVTU SFUVSO UIBU UZQF 'JOBMMZ  NFBOT JG OFJUIFS PVUQVU JT B UZQF
UIFO XF IBWF UP SFUVSO OPUIJOH *OUVJUJWFMZ XF BQQMZ UIF BSHVNFOUT UP EJĒFSFOU CSBODIFT PG
UIF PWFSMPBEFE GVODUJPO JG GBJM XF JHOPSF UIF SFTVMU BOE JG TVDDFTTGVM XF XJMM UBLF UIF SFTVMUT
PVU BOE DPNCJOF UIFN VTJOH UIF  UZQF DPOTUSVDUPS
0įĞīĥĨĚĝĢħĠ 4ĞĦĚħĭĢĜĬ *ĦĩĥĞĦĞħĭĚĭĢĨħ *U JT B SBUIFS SFTUSJDUFE GPSN PG BQQMJDBUJWFTVCUZQJOH 8F OBNF JU UIF PWFSMPBEJOH TFNBOUJDT JNQMFNFOUBUJPO TJODF JG NVMUJQMF JNQMF
NFOUBUJPOT JO BO PWFSMPBEFE EFêOJUJPO NBUDI XJUI BO BSHVNFOU XF SFKFDU UIF BQQMJDBUJPOѮJT JT TJNJMBS UP USBEJUJPOBM PWFSMPBEJOH NFDIBOJTNT XIJDI SFKFDU TVDI DBTFT BT B GPSN PG
BNCJHVJUZ *O PUIFS XPSET JO UIF PWFSMPBEJOH TFNBOUJDT POMZ POF JNQMFNFOUBUJPO DBO CF
TFMFDUFE GSPN BO PWFSMPBEFE EFêOJUJPO

A1 ! A2 = Amb

A1 ! .

= A1

. ! A2 = A2



.!.



=.



 "QQMJDBUJWF 4VCUZQJOH(Int → String)  (Bool → String) # Int

by (3.3) "→ (Int → String) # Int ! (Bool → String) # Int

by (3.1) (3.2) "→ String ! .
by (3.8) "→ String(Int → Int)  (Int → Int) # Int

by (3.3) "→ (Int → Int) # Int ! (Int → Int) # Int
by (3.1) "→ Int ! Intby (3.12) "→ Amb'JHVSF  &YBNQMFT PG "QQMJDBUJWF 4VCUZQJOH XJUI EJĒFSFOU DPNQPTJUJPO PQFSBUPSTѮF SVMF  TBZT UIBU JG UXP PVUQVUT BSF CPUI UZQFT XF SFUVSO B UZQF FSSPS K# UP EFOPUF UIFBNCJHVJUZ ѮJT SVMF NPEFMT UIF CFIBWJPVS PG PWFSMPBEJOH BNCJHVJUZ DIFDLJOH JO QSPHSBNNJOH MBOHVBHFT

3ĞĦĚīĤ ѮF BQQSPBDI PG BQQMJDBUJWF TVCUZQJOH XJUI PWFSMPBEJOH TFNBOUJDT JNQMFNFOUBUJPO JT NPSF SJHJE UIBO UIF BQQMJDBUJPO NPEF WFSTJPO ѮJT JT CFDBVTF JU XJMM SFKFDU UIF VOBNCJHVPVT BQQMJDBUJPOT MJLF 7--; R i`m2 TJODF UIF êSTU BSHVNFOU DBOOPU NBLF UIF TFMFDUJPO&ıĚĦĩĥĞĬ 8F HJWF FYBNQMFT PG PVS UXP EFTJHO PQUJPOT JO 'JHVSF  ѮF êSTU JT UIF JOGFS
FODF PG BQQMJDBUJPO UFSN b?Qr R BOE UIF SFUVSO UZQF JT ai`BM; ѮF TFDPOE JT UIF JOGFSFODF
PG BCTVSE DBTF bm++--T`2/ R BOE UIF SFTVMU JT B UZQF FSSPS K#  ѮF JEFBT BSF UP SFDVSTJWFMZ
EFMFHBUF UIF TFMFDUPS UZQF UP UIF MFѫ BOE SJHIU CSBODIFT ѮFO GPS UIF êSTU JU DPNCJOFT UIF
MFѫ BOE SJHIU SFTVMUT 'PS UIF TFDPOE JU PVUQVUT B K# TJODF CPUI CSBODIFT DBO BDDFQU UIF
BSHVNFOU XIJDI MFBET UP BNCJHVJUZϜϠ 3ĞĜĨīĝ 1īĨģĞĜĭĢĨħ*O UIJT TFDUJPO XF FNQMPZ BQQMJDBUJWF TVCUZQJOH UP SFDPSE QSPKFDUJPO BOE TIPX UIBU BQQMJDBUJWF TVCUZQJOH DBO BMTP CF VTFE UP DPNQVUF UIF SFTVMU UZQF PG QSPKFDUJPOT 3FDPSE 1SPKFDUJPO*OUFSTFDUJPO UZQFT DBO OBUVSBMMZ TVQQPSU SFDPSET XJUI B TJOHMF êFME SFDPSE UZQF BEEFE 'PS
SFDPSET XJUI NVMUJQMF êFMET XF VTF UIF JOUFSTFDUJPO UZQF DPOTUSVDUPS UP DPODBUFOBUF UIFN'PS JOTUBODF {l1 : A, l2 : B, l3 : C} JT FTTFOUJBMMZ {l1 : A}  {l2 : B}  {l3 : C}
5ZQFT

A, B ::= Int | T op | A → B | A  B | {l : A}

0SEJOBSZ 5ZQFT

Ao , B o ::= Int | T op | A → B o | {l : Ao }'VSUIFS XF JOUFHSBUF UIF SVMF 43Ĝĝ GPS SFDPSET JO UIF TVCUZQJOH {l : A} JT UIF TVCUZQF

PG {l : B} JG A JT UIF TVCUZQF PG B 5P MFU UIF JOUFSTFDUJPO UZQFT BMTP EJTUSJCVUF PWFS SFDPSEUZQFT XF FYUFOE UIF TQMJUUBCMF UZQFT XJUI UIF SFDPSE DBTF
A <: B{l : A} <: {l : B}

43Ĝĝ

A1 " A # A2
{l : A1 } " {l : A} # {l : A2 }4ĩ3Ĝĝ*O DPNQBOZ XJUI UIF SVMFT GPS JOUFSTFDUJPO UZQFT FODPEFE SFDPSE UZQFT IBWF UIF TVCUZQJOH
QSPQFSUJFT EFWFMPQFE JO DMBTTJDBM SFDPSE DBMDVMJ <$BSEFMMJ BOE .JUDIFMM > XJEUI TVCUZQJOH EFQUI TVCUZQJOH BOE QFSNVUBUJPOѮF FTTFOUJBM PQFSBUJPO GPS SFDPSET JT QSPKFDUJPO HJWFO B MBCFM BOE SFDPSE SFUVSOT UIF WBMVFT BTTPDJBUFE XJUI UIF MBCFM ѮJT QSPCMFN JT UIF TBNF XJUI UIF PWFSMPBEFE BQQMJDBUJPO HJWFO
BO BSHVNFOU BOE PWFSMPBEFE GVODUJPOT UIF SFTVMU BѫFS BQQMZJOH UIF DPSSFDU CSBODI TIPVME
CF SFUVSOFE 8F DBO SFVTF PVS BQQMJDBUJWF TVCUZQJOH CZ BCTUSBDUJOH UIF MBCFM BT TFMFDUPS UZQFTBOE FYUFOEJOH UIF OFX SVMFT 'PS SFDPSE UZQFT   XF DIFDL UIF FRVBMJUZ CFUXFFO
MBCFMT *G UIF MBCFMT BSF FRVBM XF SFUVSO UIF PVUQVU UZQF A PUIFSXJTF XF GBJM
4FMFDUPS 5ZQFT S ::= A | l
A1 → A2 # B = A2

when B <: A1

A1 → A2 # B = .

when ¬(B <: A1 )when l1 /= l2otherwise{l = A} # l = A{l1 = A} # l2 = .

A1  A2 # S = (A1 # S) ! (A2 # S)
A#S =.

&ıĚĦĩĥĞĬ 8F JMMVTUSBUF UIF JEFBT CZ FYBNQMFT {x = 1, y = i`m2}.x ѮF SFUVSO UZQF

JT AMi 8F êSTU SFDVSTJWFMZ DBMM CPUI CSBODIFT XJUI UIF TFMFDUPS UZQF MBCFM t BOE VTF UIF "QQMJDBUJWF 4VCUZQJOH
DPNQPTJUJPO PQFSBUPS UP DPNCJOF UIFJS SFTVMUT ѮF MFѫ DPNQBSFT UIF FRVBMJUZ BOE SFUVSOT JUT
BTTPDJBUFE UZQF AMi UIF SJHIU PVUQVUT B GBJMVSF TJODF MBCFM v JT OPU FRVBM UP t

{x : Int}  {y : Bool} # x

by (3.17) "→ {x : Int} # x ! {y : Bool} # x

by (3.15) (3.16) "→ Int ! .
by (3.10) "→ Int

Ϝϡ .ĞĭĚĭġĞĨīĲ
8F QSPWFE UIF TPVOEOFTT BOE DPNQMFUFOFTT PG PVS BQQMJDBUJWF TVCUZQJOH XJUI SFTQFDU UP OPSNBM TVCUZQJOH ѮF EFDJEBCJMJUZ PG BQQMJDBUJWF TVCUZQJOH JT TUSBJHIUGPSXBSE TJODF JU JT NPEFMMFE BT B TUSVDUVSBMMZ SFDVSTJWF GVODUJPO 8F IBWF UXP WFSTJPOT PG TPVOEOFTT BOE DPNQMFUF
OFTT MFNNBT ѮF êSTU WFSTJPO BQQMJFT UP UIF DBTF XIFSF UIF TVQFSUZQF JT B GVODUJPO-FNNB  4PVOEOFTT 'VODUJPO  *G A # B = C UIFO A <: B → C
1SPPG *OEVDUJPO PO UIF A # B-FNNB  $PNQMFUFOFTT 'VODUJPO  *G A <: B → C UIFO ∃D, A # B = D ∧ D <: C
1SPPG *OEVDUJPO PO UIF TVCUZQJOH A <: B → CѮF TPVOEOFTT MFNNB JT JOUVJUJWF *G UIF SFTVMU PG DIFDLJOH BQQMJDBUJWF TVCUZQJOH XJUI B TVCUZQF A BOE JOQVU UZQF B DPNQVUFT B UZQF C UIFO JU TIPVME CF UIF DBTF UIBU A <: B → C

'PS DPNQMFUFOFTT XF XJTI UP TIPX UIBU JG A JT B TVCUZQF PG B GVODUJPO UZQF B → C UIFOBQQMJDBUJWF TVCUZQJOH XJMM BMXBZT CF BCMF UP êOE TPNF PVUQVU UZQF D XIJDI JT B TVCUZQF PGCѮF TFDPOE WFSTJPO PG UIF MFNNB XIJDI BQQMJFT UP UIF DBTF XIFSF UIF TVQFSUZQF JT B SFDPSEJT EFêOFE JO B TJNJMBS NBOOFS-FNNB  4PVOEOFTT 3FDPSE  *G A # l = B UIFO A <: {l : B}
-FNNB  $PNQMFUFOFTT 3FDPSE  *G A <: {l : B} UIFO ∃C, A # l = C ∧ C <: B .FUBUIFPSZ
3ĞĦĚīĤ /PUF UIBU JG XF XPVME ESPQ UIF EJTUSJCVUJWJUZ PG JOUFSTFDUJPOT PWFS PUIFS DPOTUSVDUT CZ SFNPWJOH UIF SVMFT 4ĩ"īī BOE 4ĩ3Ĝĝ UIFO UP IBWF TPVOEOFTT BOE DPNQMFUF
OFTT XF OFFE UP FNQMPZ UIF DPNQPTJUJPO PQFSBUPS JNQMFNFOUJOH UIF PWFSMPBEJOH TFNBOUJDT8IFO VTJOH UIBU DPNQPTJUJPO PQFSBUPS UIF TPVOEOFTT MFNNBT SFNBJO UIF TBNF CVU XF OFFE
UP BEKVTU UIF DPNQMFUFOFTT MFNNBT UP DPOTJEFS UIF BNCJHVPVT DBTFT 'PS JOTUBODF UIF DPNQMFUFOFTT GPS UIF DBTF PG B GVODUJPO TVQFSUZQF XPVME CFDPNF
-FNNB  $PNQMFUFOFTT  *G A <: B → C UIFO (∃D, A # B = D ∧ D <: C) ∨ A #B = Ambϝ " $ĚĥĜĮĥĮĬ İĢĭġ "ħ 6ħīĞĬĭīĢĜĭĞĝ .ĞīĠĞ
0ĩĞīĚĭĨī

ѮJT TFDUJPO QSFTFOUT B UZQF TPVOE DBMDVMVT UIBU TVQQPSUT CPUI JOUFSTFDUJPO UZQFT BOE B NFSHF
PQFSBUPS ѮJT DBMDVMVT DBO CF WJFXFE BT B WBSJBOU PG %VOêFMET DBMDVMVT XJUIPVU VOJPO UZQFT<%VOêFME > 0VS DBMDVMVT FNQMPZT B UZQFEJSFDUFE PQFSBUJPOBM TFNBOUJDT <)VBOH FU BM
> JOTUFBE PG VTJOH FMBCPSBUJPO TFNBOUJDT BT QSPQPTFE CZ %VOêFME BOE BEPQUT BQQMJDBUJWF TVCUZQJOH BOE EJTUSJCVUJWF TVCUZQJOH 0WFSMPBEFE GVODUJPOT OFTUFE DPNQPTJUJPO BOE
NVMUJêFME SFDPSET DBO BMM CF FODPEFE JO UIJT DBMDVMVT *O DPOUSBTU JO %VOêFMET DBMDVMVT
EJTUSJCVUJWJUZ BOE OFTUFE DPNQPTJUJPO BSF OPU TVQQPSUFE -JLF %VOêFMET DBMDVMVT UIF QSFTFODF PG VOSFTUSJDUFE NFSHFT NBLFT UIF TFNBOUJDT OPOEFUFSNJOJTUJD 8F BEESFTT UIF JTTVF PG
OPOEFUFSNJOJTN JO UIF OFYU TFDUJPOϝϚ 4ĲħĭĚı
ѮF TZOUBY PG UIJT DBMDVMVT JT
&YQSFTTJPOT3BX 7BMVFT
7BMVFT$POUFYUTe ::= x | i | e : A | e1 e2 | λx .e : A → B | e1 , , e2 | {l = e} | e.l
p ::= i | λx .e : A → B

v ::= p : Ao | v1 , , v2 | {l = v}
Γ ::= · | Γ, x : A.PTU FYQSFTTJPOT BSF TUBOEBSE ѮF MBNCEB FYQSFTTJPO λx. e : A → B JT GVMMZ BOOPUBUFECFDBVTF UIF PQFSBUJPOBM TFNBOUJDT JT UZQFEJSFDUFE ѮF FYQSFTTJPO e1 , , e2 DSFBUFT B NFSHF PG
UXP FYQSFTTJPOT e1 BOE e2  ѮF FYQSFTTJPO {l = e} EFOPUFT B TJOHMFêFME SFDPSE XJUI MBCFM l

BOE êFME e ѮF QSPKFDUJPO PG SFDPSET JT SFQSFTFOUFE CZ e.l $POUFYUT BSF TUBOEBSE Γ JT B MJTU
PG CPVOE WBSJBCMFT x BOE UIFJS UZQFT A
3BX WBMVFT JODMVEF JOUFHFST BOE MBNCEBT BOE WBMVFT BSF EFêOFE PO SBX WBMVFT BOOPUBUFEXJUI PSEJOBSZ UZQFT NFSHFT PG WBMVFT BOE SFDPSET XIPTF êFMET BSF WBMVFT 8F TUSBUJGZ SBXWBMVFT BOE WBMVFT CFDBVTF XF OFFE UP VUJMJTF BOOPUBUJPOT UP BEPQU EJTQBUDIJOH JO UIF TFNBO

 " $BMDVMVT XJUI "O 6OSFTUSJDUFE .FSHF 0QFSBUPS#JEJSFDUJPOBM 5ZQJOH

Γ'e⇔A
5-Ģĭ

Γ ' J ⇒ AMi
53Ĝĝ

Γ'e⇒A

Γ ' {M = e} ⇒ {M : A}
51īĨģ

Γ'e⇒A

A#M=B

Γ ' e.M ⇒ B

57Ěī

5-ĚĦ

Γ'Y⇒A

Γ ' λY. e : A → B ⇒ A → B

x:A ∈ Γ5"ĩĩ

Γ ' e ⇒ A

Γ, Y : A ' e ⇐ B

Γ ' e ⇒ B

Γ ' e e ⇒ C

5.īĠ

Γ ' e ⇒ A

Γ ' e ⇒ B

Γ ' e , , e ⇒ A  B

A#B=C
5"ħħ

Γ'e⇐A

Γ'e:A⇒A

54Įě

Γ'e⇒A

A <: BΓ'e⇐B'JHVSF  #JEJSFDUJPOBM 5ZQJOHUJDT ѮF PSEJOBSZ SFTUSJDUJPO PO WBMVFT FOGPSDFT B DBOPOJDBM GPSN GPS PWFSMPBEFE GVODUJPOT0WFSMPBEFE GVODUJPOT XJMM CF SFEVDFE UP FYQMJDJU OFTUFE NFSHFT FWFO JO TFUUJOHT XJUI EJTUSJCVUJWJUZϝϛ 5ĲĩĢħĠ
'JHVSF  TIPXT PVS CJEJSFDUJPOBM UZQF TZTUFN .PTU PG UIF SVMFT BSF BEBQUFE GSPN USBEJUJPOBM CJEJSFDUJPOBM UZQJOH <%VOêFME BOE ,SJTIOBTXBNJ > ѮF OPWFM SVMFT BSF SVMFT 5
"ĩĩ BOE 51īĨģ XIPTF JOGFSSFE UZQF JT EFSJWFE GSPN BQQMJDBUJWF TVCUZQJOHϝϛϚ 5ĲĩĢħĠ Ĩğ "ĩĩĥĢĜĚĭĢĨħ Ěħĝ 1īĨģĞĜĭĢĨħ
ѮF DPNNPO BQQSPBDI UP UZQJOH BQQMJDBUJPOT JT UP JOGFS UIF GVODUJPO UZQF êSTU VTF UIF JOQVUUZQF UP DIFDL UIF BSHVNFOUT BOE BTTJHO UIF PVUQVU UZQF UP BQQMJDBUJPOT 0VS BQQSPBDI UPUZQF BQQMJDBUJPOT <9JF BOE 0MJWFJSB > JT UP JOGFS UZQF PG GVODUJPOT BOE BSHVNFOUT BU UIFTBNF UJNF QBTT UIFJS UZQFT JOUP BQQMJDBUJWF TVCUZQJOH A BOE B JO SVMF 5"ĩĩ BOE BTTJHO UIFDPNQVUFE SFTVMU C UP BQQMJDBUJPOT ѮJT JT CFDBVTF XF BMMPX JOUFSTFDUJPO UZQFT UP EJTUSJCVUFPWFS BSSPX UZQFT UIVT UIF UZQF PG UIF GVODUJPO DBO CF BO BSSPX UZQF PS BO JOUFSTFDUJPO UZQF
8F DBOOPU TJNQMZ FYUSBDU UIF JOQVU UZQF PG B GVODUJPO 4JODF NVMUJêFME SFDPSET BSF BMTP 4FNBOUJDTJOUFSTFDUJPO UZQFT JO PVS TZTUFN UIF UZQJOH GPS QSPKFDUJPOT SVMF 51īĨģ VTFT B TJNJMBS JEFBUP BQQMJDBUJPOT 8F JOGFS UIF UZQFT PG e BOE HFU UIF MBCFM l QBTT JU UP BQQMJDBUJWF TVCUZQJOH BOE
EFSJWF UIF SFTVMU UZQF GPS QSPKFDUJPOTϝϛϛ &ıĚĦĩĥĞĬ
8F TIPX BO FYBNQMF PG IPX UIF SVMF 5"ĩĩ XPSLT 4VQQPTF UIBU XF IBWF Γ = f : I → I →I, g : I → B → B I BOE B TUBOE GPS AMi BOE "QQH

Γ ' U7--;V ⇒ (I → I → I)  (I → B → B)

Γ ' U7--;V k ⇒ (I → I)  (B → B)
Γ ' U7--;V k i`m2 ⇒ B

Γ'2⇒I

5"ĩĩ
Γ ' i`m2 ⇒ B

5"ĩĩ

5P JOGFS UIF UZQF PG U7--;V k i`m2 XF êSTU JOGFS CPUI UIF UZQF PG U7--;V k BOE i`m2 ѮF
UZQF PG U7--;V k JT UAMi → AMiV  U"QQH → "QQHV ѮJT SFTVMU JT DPNQVUFE GSPN BQQMJDBUJWF TVCUZQJOH XJUI UXP JOQVUT UZQF PG GVODUJPO NFSHFT 7--; BOE UZQF PG k -BUFS XF
VTF UIF DPNQVUFE SFTVMU PG U7--;V k UP EFSJWF PVS êOBM UZQF "QQHϝϛϜ 1īĨĩĞīĭĢĞĬ Ĩğ 5ĲĩĢħĠ
4JODF PVS UZQJOH SVMFT BEPQU UFDIOJRVFT PG CJEJSFDUJPOBM UZQJOH UIFSF BSF TPNF QSPQFSUJFT-FNNB  6OJRVFOFTT PG 4ZOUIFTJT  *G Γ ' e ⇒ A BOE Γ ' e ⇒ B UIFO A = B-FNNB  $IFDLJOH 4VCTVNQUJPO  *G Γ ' e ⇐ A BOE A ≤ B UIFO Γ ' e ⇐ BϝϜ 4ĞĦĚħĭĢĜĬ
ѮJT DBMDVMVT BEPQUT B UZQFEJSFDUFE PQFSBUJPOBM TFNBOUJDT <)VBOH FU BM > XIFSF UZQF
BOOPUBUJPOT BSF VTFE UP DBTU UFSNT JOTUFBE PG CFJOH FSBTFE BѫFS UZQF DIFDLJOHϝϜϚ $ĚĬĭĢħĠ
8F JOUSPEVDF UIF DBTUJOH KVEHNFOU JO 'JHVSF  +VEHNFOU v )−→A v " EFTDSJCFT UIBU WBMVFv JT DBTU UP BOPUIFS WBMVF v " CZ UZQF A UIVT GPSDJOH UIF WBMVF UP NBUDI UIF UZQF TUSVDUVSF PG
A ѮF DBTUJOH SVMFT BSF FTTFOUJBMMZ UIF TBNF BT UIF SVMFT QSPQPTFE CZ )VBOH FU BM <>
3VMFT $ĭ.īĠ- BOE $ĭ.īĠ3 TUBUF UIBU NFSHFT XJMM CF DBTU UP POF SFTVMU CZ PSEJOBSZ UZQFT'PS FYBNQMF b?QrAMi--b?Qr"QQH XJMM CF DBTU UP b?QrAMi CZ UZQF AMi → ai`BM;
-FNNB  1SFTFSWBUJPO PG $BTUJOH  *G Γ ' v ⇒ B BOE v )−→A v " UIFO Γ ' v " ⇐ A " $BMDVMVT XJUI "O 6OSFTUSJDUFE .FSHF 0QFSBUPS$BTUJOHv )−→A v "$ĭ*ħĭ

$ĭ5Ĩĩ

J : A )−→AMi J : AMiv )−→hQT . : hQT$ĭ"īī

$ĭ3Ĝĝ

v )−→Ao v "{M = v} )−→{M:Ao } {M = v " }$ĭ.īĠ-E <: C → Do

(λY. e : A → B) : E )−→(C→Do ) (λY. e : A → Do ) : (C → Do )$ĭ.īĠ3v )−→Ao v"v , , v )−→Ao$ĭ"ħĝ

A " A # Av"v )−→A vv )−→A v , , vv )−→Ao v"v , , v )−→Ao v"v )−→A v

'JHVSF  $BTUJOHѮF QSFTFSWBUJPO PG DBTUJOHT TUBUFT UIBU UIF TUSVDUVSF PG UIF DBTU SFTVMU v " XJMM NBUDI UIF UZQFQSPWJEFE-FNNB  1SPHSFTT PG $BTUJOH  *G · ' v ⇐ A UIFO ∃v " , v )−→A v " ѮF QSPHSFTT MFNNB PG DBTUJOHT TUBUFT UIBU B XFMMUZQFE WBMVF DBO CF DBTU UP BOPUIFS WBMVF
.PSF TQFDJêDBMMZ JG UIJT WBMVF DBO CF DIFDLFE CZ UIF UZQF A UIFO JU DBO CF DBTU CZ UIF UZQF
A 'PS FYBNQMF b?QrAMi--b?Qr"QQH DBO CF DIFDLFE CZ UIF UZQF AMi → ai`BM; UIFO JU DBO
CF DBTU CZ UIJT UZQF

ϝϜϛ "ĩĩĥĢĜĚĭĢįĞ %ĢĬĩĚĭĜġĢħĠ
8F JOUSPEVDF B OFX KVEHFNFOU DBMMFE BQQMJDBUJWF EJTQBUDIJOH 'JHVSF  XIJDI FYUFOET)VBOH FU BM <> QBSBMMFM BQQMJDBUJPO KVEHFNFOU ѮF JEFB PG UIF QBSBMMFM BQQMJDBUJPO JT
TJNQMF GVODUJPO NFSHFT XJMM CF QBSBMMFM BQQMJFE UP BSHVNFOUT *O DPOUSBTU UP QBSBMMFM BQQMJDBUJPO XF NVTU BMTP EFBM XJUI PWFSMPBEJOH +VEHNFOU (v • vl) "→ e EFTDSJCFT UIBU WBMVF v JT
BQQMJFE UP TFMFDUPST vl BOE UIFO SFEVDFE UP B UFSN e

4FMFDUPST vl ::= v | l
3VMF "ĩĩ-ĚĦ QFSGPSNT CFUBSFEVDUJPO BOE BQQFOET BO FYUSB BOOPUBUJPO D UP FOGPSDF UIFPVUQVU UZQF PG UIF BQQMJDBUJPO 3VMF "ĩĩ1īĨģ TJNQMZ FYUSBDUT UIF WBMVF GSPN UIF TJOHMF
SFDPSE êFME ѮF JOUFSFTUJOH QBSU JT UIF SFNBJOJOH UISFF SVMFT GPS NFSHFT ѮF GVODUJPO 1vl2

TJNQMZ FYUSBDUT PVU UIF UZQF PG B WBMVF PS B MBCFM UP QSPWJEF UIF UZQFT UP CF DPNQBSFE XJUI 4FNBOUJDT"QQMJDBUJWF %JTQBUDIJOH(v • vl) "→ e"ĩĩ-ĚĦ

"ĩĩ1īĨģ

v )−→A v "((λY. e : A → B) : C → D • v) "→ e[Y )→ v " ] : D"ĩĩ.īĠ-1v2 2 # 1vl2 = .

(v • vl) "→ e"ĩĩ.īĠ3

1v1 2 # 1vl2 = .

(v • vl) "→ e(v • vl) "→ e(v • vl) "→ e((v , , v ) • vl) "→ e"ĩĩ.īĠ1

1v1 2 # 1vl2 /= .

1v2 2 # 1vl2 /= .

({M = v} • M) "→ v((v , , v ) • vl) "→ e((v , , v ) • vl) "→ e , , e

'JHVSF  "QQMJDBUJWF %JTQBUDIJOH

BQQMJDBUJWF TVCUZQJOH 'PS MBCFM 1l2 TJNQMZ SFUVSOT UIF PSJHJOBM WBMVF BOE GPS WBMVFT 1v2
FYUSBDUT UIF BOOPUBUJPO GSPN UFSNT *U DBO CF EFêOFE BT B TUSVDUVSBMMZ SFDVSTJWF GVODUJPO
1l2 = l1p : Ao 2 = Ao

1v1 , , v2 2 = 1v1 2  1v2 2
1{l = v}2 = {l : 1v2}
5P EFBM XJUI PWFSMPBEJOH XF OFFE UP JOUSPEVDF SVMFT "ĩĩ.īĠ- BOE "ĩĩ.īĠ3 XIJDIBMMPXT B NFSHF UP CF BQQMJFE XIFO POMZ POF PG UIF WBMVFT JT BQQMJDBCMF ѮF MBTU SVMF SVMF "ĩĩ.īĠ1 EFBMT XJUI UIF QBSBMMFM BQQMJDBUJPO XIFSF CPUI WBMVFT JO UIF NFSHF DBO CF BQQMJFE-FNNB  1SFTFSWBUJPO PG "QQMJDBUJWF %JTQBUDIJOH 'VODUJPO BOE 3FDPSET 
t *G · ' v1 v2 ⇒ A BOE v1 • v2 "→ e UIFO · ' e ⇐ At *G · ' v.l ⇒ A BOE v • l "→ e UIFO · ' e ⇐ AѮF QSFTFSWBUJPO MFNNB PG BQQMJDBUJWF EJTQBUDIJOH TUBUFT UIBU GPS B XFMMUZQFE BQQMJDBUJPO PSQSPKFDUJPO UFSN UIFJS UZQFT XJMM CF QSFTFSWFE JO UIF FWBMVBUJPO PG UIF BQQMJDBUJWF EJTQBUDIJOH
KVEHNFOU-FNNB  1SPHSFTT PG "QQMJDBUJWF %JTQBUDIJOH 'VODUJPO BOE 3FDPSET 
t *G · ' v1 v2 ⇒ A UIFO ∃e, v1 • v2 "→ e " $BMDVMVT XJUI "O 6OSFTUSJDUFE .FSHF 0QFSBUPS
4NBMM4UFQ 3FEVDUJPOe )−→ e"4ĭĞĩ"ĩĩ4ĭĞĩ*ħĭ"ħħ

4ĭĞĩ"īī"ħħJ )−→ J : AMi

λY. e : A → B )−→ (λY. e : A → B) : A → B

4ĭĞĩ1į4ĩĥĢĭ

4ĭĞĩ1īģ

p : A )−→ p : A , , p : Av.M )−→ v "A " A # A(v • M) "→ v "(v • v ) "→ ev v )−→ e

4ĭĞĩ"ħħ¬e ∈ pe )−→ e"e : A )−→ e" : A

4ĭĞĩ7Ěĥ"ħħ

4ĭĞĩ"ĩĩ-4ĭĞĩ"ĩĩ34ĭĞĩ.īĠ-v : A )−→ v "e e )−→ e" ev e )−→ v e"

e , , e )−→ e" , , ev )−→A v "e )−→ e"

e )−→ e"

e )−→ e"

4ĭĞĩ.īĠ3

4ĭĞĩ3Ĝĝ3

4ĭĞĩ1īģ-v , , e )−→ v , , e"

{M = e} )−→ {M = e" }e.M )−→ e" .Me )−→ e"e )−→ e"e )−→ e"'JHVSF  0QFSBUJPOBM 4FNBOUJDTt *G · ' v.l ⇒ A UIFO ∃e, v • l "→ eѮF QSPHSFTT MFNNB PG BQQMJDBUJWF EJTQBUDIJOH TUBUFT UIBU XFMMUZQFE BQQMJDBUJPO PS QSPKFDUJPOUFSNT BSF BCMF UP CF FWBMVBUFE CZ UIF BQQMJDBUJWF EJTQBUDIJOH KVEHNFOUϝϜϜ 0ĩĞīĚĭĢĨħĚĥ 4ĞĦĚħĭĢĜĬ
8F QSFTFOU PVS TNBMMTUFQ SFEVDUJPO SVMFT JO 'JHVSF  3VMFT 4ĭĞĩ*ħĭ"ħħ BOE 4ĭĞĩ"īī"ħħ BQQFOE FYUSB BOOPUBUJPOT UP UIF QBSUJBM WBMVF JO PSEFS UP QSFTFSWF UIF QSFDJTF UZQFT BU
SVOUJNF 3VMF 4ĭĞĩ1į4ĩĥĢĭ XJMM TQMJU UFSNT BDDPSEJOH UP TQMJUUBCMF UZQFT GPSDJOH UIF UZQF PGFBDI CSBODI JO NFSHFT UP CF PSEJOBSZ 3VMFT 4ĭĞĩ"ĩĩ BOE 4ĭĞĩ1īģ EJSFDUMZ DBMM BQQMJDBUJWFEJTQBUDIJOH 3VMF 4ĭĞĩ7Ěĥ"ħħ USJHHFST DBTUJOH v JT DBTU UP v " CZ UZQF A 3VMF 4ĭĞĩ"ħħ
JT B DPOHSVFODF SVMF XJUI B SFTUSJDUJPO UIBU e DBOOPU CF B SBX WBMVF p ѮF SFNBJOJOH SVMFTBSF OPSNBM DPOHSVFODF SVMFTϝϝ 5ĲĩĞ 4ĨĮħĝħĞĬĬ
8F TIPX UIF QSFTFSWBUJPO MFNNBT PG DBTUJOH BOE BQQMJDBUJWF EJTQBUDIJOH VTJOH UIF DIFDLJOH
NPEF ѮBU JT UP TBZ UIF UZQFT BSF OPU FYBDUMZ QSFTFSWFE JO UIF FWBMVBUJPO *OTUFBE XF DBO
POMZ FOTVSF UIBU UZQFT DBO CFDPNF TNBMMFS BOE JT UIF TVCUZQF PG PSJHJOBM UZQFT )PXFWFS PVS 5ZQF 4PVOEOFTT*TPNPSQIJD 4VCUZQJOH

A≈B*4Įě3Ğğĥ

A≈A*4Įě3Ĝĝ

A≈B*4Įě"ħĝB " B # B{M : A} ≈ {M : B}A ≈ BA  A ≈ B

A ≈ B 'JHVSF  *TPNPSQIJD 4VCUZQJOHDBMDVMVT JT NPSF TUSJDU UIBO UIBU UIF JTPNPSQIJD GPSN PG UIF UZQFT XJMM CF QSFTFSWFE JO UIFSFEVDUJPO 8F TIPX UIF JTPNPSQIJD TVCUZQJOH JO 'JHVSF  BOE QSPWF B NPSF TUSJDU WFSTJPOPG QSFTFSWBUJPOϝϝϚ *ĬĨĦĨīĩġĢĜ 4ĮěĭĲĩĢħĠ*TPNPSQIJD TVCUZQJOH JT B SFTUSJDUFE SFMBUJPO UP EFTDSJCF SFMBUJPOT CFUXFFO UZQFT 8F TIPXUIF SVMFT JO 'JHVSF  3VMF *ĬĮě3Ğğĥ EFTDSJCFT UIBU UZQFT BSF JTPNPSQIJD XJUI UIFNTFMWFT
3VMF *ĬĮě3Ĝĝ HJWFT B TQFDJBM USFBUNFOU GPS SFDPSE UZQFT {l : A} ≈ {l : B} JG A ≈ BѮF SFBTPO XIZ XF EJTUJOHVJTI GVODUJPO UZQFT BOE SFDPSE UZQFT IFSF JT UIBU XF IBWF TMJHIUMZEJĒFSFOU FWBMVBUJPO TUSBUFHJFT GPS GVODUJPOT BOE SFDPSET 'PS GVODUJPOT XF BQQFOE BO BOOPUBUJPO UP JU BOE NBLF B TQMJU JG BQQMJDBCMF 'PS SFDPSET XF FWBMVBUF UIF JOOFS FYQSFTTJPO JOUPWBMVFT 3VMF *ĬĮě"ħĝ DBQUVSFT UIF FTTFODF PG UIF JTPNPSQIJD TVCUZQJOH UIF JOUFSTFDUJPOUZQFT BSF JTPNPSQIJD TVCUZQJOH UP UIFJS DPSSFTQPOEJOH TQMJUUBCMF UZQFT 'PS FYBNQMF UAMi
→ ai`BM;V  UAMi → "QQHV JT JTPNPSQIJD TVCUZQJOH UP AMi → Uai`BM;  "QQHVѮF JTPNPSQIJD TVCUZQJOH IBT UIF GPMMPXJOH QSPQFSUJFT-FNNB  5SBOTJUJWJUZ PG *TPNPSQIJD 4VCUZQJOH  *G A ≈ B BOE B ≈ C UIFO A ≈ C1SPPG *OEVDUJPO PO UIF TJ[F PG UIF UZQF B
-FNNB  4PVOEOFTT PG *TPNPSQIJD 4VCUZQJOH  *G A ≈ B UIFO A <: B BOE B <: A
-FNNB  "QQMJDBUJWF 4VCUZQJOH BOE *TPNPSQIJD 4VCUZQJOH 'VODUJPO BOE 3FDPSET 
t *G A # B = C A" ≈ A BOE B " ≈ B UIFO ∃C " , A" # B " = C " ∧ C " ≈ Ct *G A # l = B A" ≈ A UIFO ∃B " , A" # l = B " ∧ B " ≈ Bϝϝϛ 5ĲĩĞ 4ĨĮħĝħĞĬĬ
5ZQF TPVOEOFTT JT QSPWFO WJB TUBOEBSE QSFTFSWBUJPO BOE QSPHSFTT UIFPSFNT " $BMDVMVT XJUI "O 6OSFTUSJDUFE .FSHF 0QFSBUPSćFPSFN  1SFTFSWBUJPO  *G · ' e ⇔ A BOE e )−→ e" UIFO · ' e" ⇒ A" ∧ A" ≈ AćFPSFN  1SPHSFTT  *G · ' e ⇔ A UIFO e JT B WBMVF PS ∃e" , e )−→ e" 
$PSPMMBSZ  5ZQF 4PVOEOFTT  *G · ' e ⇔ A BOE e )−→∗ e" UIFO e" XJMM OPU HFU TUVDLϞ " $ĚĥĜĮĥĮĬ İĢĭġ " %ĢĬģĨĢħĭ .ĞīĠĞ
0ĩĞīĚĭĨī

ѮJT TFDUJPO QSFTFOUT B TFDPOE DBMDVMVT XJUI B EJTKPJOUOFTT SFTUSJDUJPO PO NFSHFT <0MJWFJSBFU BM > UP SFDPWFS EFUFSNJOJTN ѮJT DBMDVMVT GPSCJET TPNF DBTFT PG DPOWFOUJPOBM PWFSMPBEJOH CVU TUJMM TVQQPSUT UIF PUIFS GFBUVSFT 8F GPDVT PO UIF LFZ EJĒFSFODFT GSPN UIF QSFWJPVT DBMDVMVT TJODF NPTU SVMFT BOE SFMBUJPOT BSF UIF TBNF $PNQBSFE UP QSFWJPVT DBMDVMJXJUI EJTKPJOU JOUFSTFDUJPO UZQFT UIF NBJO OPWFMUZ JT UIF VTF PG UIF BQQMJDBUJWF TVCUZQJOH BOE
EJTQBUDIJOH SFMBUJPOT XIJDI FOBCMFT TVQQPSU GPS SFDPSE QSPKFDUJPOT BOE B SFTUSJDUFE GPSN PG
PWFSMPBEJOH OBUVSBMMZ XJUIPVU SFEVOEBOU UZQF BOOPUBUJPOT ϞϚ %ĢĬģĨĢħĭħĞĬĬ
8F FNQMPZ UIF EFêOJUJPO PG EJTKPJOUOFTT QSPQPTFE CZ 0MJWFJSB FU BM <> *OGPSNBMMZ JG BMMDPNNPO TVQFSUZQFT PG UXP UZQFT BSF UPQMJLF UZQFT XF DBO DPODMVEF UIBU UIF UXP UZQFT BSF
EJTKPJOU 5PQMJLF UZQFT BSF UIPTF UIBU BSF TVQFSUZQFT PG BMM UZQFT FH hQT hQT  hQT BOEEFêOFE JO 'JHVSF ѮF JODMVTJPO PG TVDI UZQFT JOUP UPQMJLF UZQFT JT BMTP QBSU PG UIF DMBTTJDBM #$% TVCUZQJOHSFMBUJPO <#BSFOESFHU FU BM > " GPSNBM TQFDJêDBUJPO PG EJTKPJOUOFTT JT HJWFO CFMPX ѮFSF
JT B TPVOE BOE DPNQMFUF TFU PG BMHPSJUINJD EJTKPJOUOFTT SVMFT UIBU DPOGPSN UP UIJT TQFDJêDB
UJPO 8F QSFTFOU JU JO 'JHVSF %FĕOJUJPO  %JTKPJOUOFTT  A ∗ B % ∀C JG A <: C ∧ B <: C UIFO C JT UPQMJLF

*O PVS DBMDVMVT XF BMMPX NFSHFT PG EJTKPJOU GVODUJPOT BOE UZQFT TVDI BT AMi → AMi PS AMi→ "QQH BSF EJTKPJOU 5P JODMVEF GVODUJPO UZQFT JOUP PVS EJTKPJOUOFTT UZQFT MJLF AMi →hQT TIPVME CF UPQMJLF BOE TVQFSUZQFT PG BMM UZQFT TJODF PUIFSXJTF AMi → AMi BOE AMi →"QQH DBOOPU CF EJTKPJOU BDDPSEJOH UP PVS EFêOJUJPO 8F GPMMPX QSFWJPVT XPSL PO EJTKPJOUJOUFSTFDUJPO UZQFT <#J FU BM > BOE HFOFSBMJ[F PVS TVCUZQJOH SVMF GPS SVMF 45Ĩĩ
45Ĩĩ

6B7
A <: B " $BMDVMVT XJUI " %JTKPJOU .FSHF 0QFSBUPS
5PQMJLF 5ZQFT

6A7
5ĥ"ħĝ

5ĥ5Ĩĩ

6A7

6B7

6A  B76hQT7

5ĥ"īī

5ĥ3Ĝĝ

6A → B7

6{M : A}7

6B7

6A7

'JHVSF  5PQMJLF UZQFT%JTKPJOUOFTTA∗B%ģ5Ĩĩ-%ģ5Ĩĩ3%ģ*ħĭ"īī%ģ"īī*ħĭ

hQT ∗ AA ∗ hQT

AMi ∗ A → B

A → B ∗ AMi%ģ3Ĝĝ&ĪA∗B{M : A} ∗ {M : B}%ģ3Ĝĝ/ĞĪ

M /= M%ģ3Ĝĝ"īī

A → B ∗ {M : C}

{M : A} ∗ B → C

B∗D

A→B∗C →D%ģ*ħĭ3Ĝĝ%ģ3Ĝĝ*ħĭ

AMi ∗ {M : A}

{M : A} ∗ AMi{M : A} ∗ {M : B}%ģ"īī3Ĝĝ

%ģ"īī"īī%ģ"ħĝ-A∗C%ģ"ħĝ3

B∗C

AB ∗ CA∗B

A∗CA ∗ B C'JHVSF  "MHPSJUINJD %JTKPJOUOFTT%JTKPJOUOFTT IBT JNQPSUBOU QSPQFSUJFT XIJDI BSF IFMQGVM GPS UIF NFUBUIFPSZ PG DBMDVMVT *O
QBSUJDVMBS JG UXP UZQFT BSF EJTKPJOU UIFJS BQQMJDBUJWF TVCUZQJOH SFTVMUT VOEFS UIF TBNF QBSUJBMUZQFT BSF BMTP EJTKPJOU-FNNB  $PWBSJBODF PG %JTKPJOUOFTT  *G A ∗ B BOE B <: C UIFO A ∗ C-FNNB  "QQMJDBUJWF 4VCUZQJOH BOE %JTKPJOUOFTT  *G A ∗ B A # S = C1 BOE B #S = C2 UIFO C1 ∗ C2 Ϟϛ %ĢĬģĨĢħĭħĞĬĬ Ěħĝ "ĩĩĥĢĜĚĭĢįĞ 4ĮěĭĲĩĢħĠ
8JUI UIF NPSF HFOFSBM TVCUZQJOH SVMF GPS UPQMJLF UZQFT BQQMJDBUJWF TVCUZQJOH SFNBJOT TPVOEXJUI -FNNB  -FNNB  JO $IBQUFS  XJUI SFTQFDU UP TVCUZQJOH )PXFWFS UIF DPNQMFUFOFTT PG PVS BQQMJDBUJWF TVCUZQJOH OFFET UP CF TMJHIUMZ BEBQUFE 5ZQJOH-FNNB  $PNQMFUFOFTT PG "QQMJDBUJWF 4VCUZQJOH  *G A <: B → C UIFO (∃D, A #B = D ∧ D <: C) ∨ T op <: C

*O PUIFS XPSET BQQMJDBUJWF TVCUZQJOH JT DPNQMFUF FYDFQU GPS UIF DBTF XIFSF UIF PVUQVU UZQF
JT UPQMJLF *O TVDI DBTF BQQMJDBUJWF TVCUZQJOH GBJMT /PUF UIPVHI UIBU UIJT GBJMVSF QSFWFOUT
TUSBOHF QSPHSBNT GSPN CFJOH UZQFDIFDLFE 'PS FYBNQMF TVCUZQJOH IBT JOTUBODFT hQT I,
 → hQT BMMPXJOH UR , hQTV k UP CF XFMMUZQFE XIJDI XPVME SFRVJSF TQFDJBM USFBUNFOU JOUIF UZQJOH SVMFT 8F SFKFDU TVDI DBTFT NBLJOH UIF UZQJOH SVMFT TJNQMFS BOE BWPJEJOH UZQF
DIFDLJOH TVDI QSPHSBNTϞϜ 5ĲĩĢħĠѮF NBJO DIBOHF JO UZQJOH JT UIBU XF BEE B EJTKPJOU QSFNJTF JO SVMF 5.īĠ 8F TIPX UIF GVMMUZQJOH SVMFT JO 'JHVSF  4QFDJBMMZ SVMF 5.īĠ7Ěĥ JT VTFE UP QSPWF UIF DPOTJTUFODZ PG UIFFWBMVBUJPO BOE DBO CF JHOPSFE JO UIF JNQMFNFOUBUJPOΓ ' e1 ⇒ A

Γ ' e2 ⇒ B

Γ ' e1 , , e 2 ⇒ A  B

A∗B

5.īĠ

3ĞĦĚīĤ %JTKPJOUOFTT IBT JUT BEWBOUBHF PWFS UIF DPIFSFODF QSPQFSUZ IPXFWFS JU SFKFDUTTPNF VTFGVM GVODUJPOT TVDI BT b?Qr ѮF TJEF DPOEJUJPO A ∗ B GPSCJET UIF UFSN UZQFE XJUIUAMi → ai`BM;V  U"QQH → ai`BM;V TJODF UIFZ BSF OPU EJTKPJOU BDDPSEJOH UP UIF EFêOJUJPO JO 'JHVSF Ϟϝ %ĲħĚĦĢĜ 4ĞĦĚħĭĢĜĬ
.PTU DIBOHFT JO UIF EZOBNJD TFNBOUJDT BSF SFMBUFE UP UPQMJLF UZQFT #BTJDBMMZ XF OFFE TPNF
FYUSB DPOEJUJPOT JO UIF SVMFT UFTUJOH XIFUIFS PS OPU UZQFT BSF UPQMJLF )PXFWFS BQBSU GSPN
UIFTF NJOPS DIBOHFT UIF SVMFT SFNBJO FTTFOUJBMMZ UIF TBNF 8F TIPX UXP KVEHNFOUT JO 'JH
VSF  BOE 'JHVSF 4JODF PVS WBMVF EFêOFT BT SBX WBMVFT DBSSZJOH BOOPUBUJPO UIF TQFDJBM UFSN GPS hQT JT VO
OFDFTTBSZ TJODF XF DBO VTF BOZ DPOTUBOU UFSNT 1 JO PVS SVMFT XJUI UPQMJLF UZQFT UP SFQMBDFUIFN 3VMF $ĭ5Ĩĩ TBZT UIBU WBMVFT XJMM CF DBTU UP B DPOTUBOU WBMVF 1 : Ao XF EFNPOTUSBUF
1 IFSF GPS TJNQMJDJUZ CZ BO PSEJOBSZ UPQMJLF UZQF

 " $BMDVMVT XJUI " %JTKPJOU .FSHF 0QFSBUPS#JEJSFDUJPOBM 5ZQJOH

Γ'e⇔A
5-Ģĭ

5-ĚĦ

Γ'Y⇒A

Γ ' λY. e : A → B ⇒ A → B

x:A ∈ ΓΓ ' J ⇒ AMi
53Ĝĝ

57Ěī

5"ĩĩ

Γ'e⇒A

Γ ' e ⇒ A

Γ ' {M = e} ⇒ {M : A}
51īĨģ

· ' u ⇒ A

Γ ' e e ⇒ C

Γ ' e ⇒ A

A#B=C

Γ ' e ⇒ B

Γ ' e , , e  ⇒ A  B

Γ ' e.M ⇒ B

5.īĠ7ĚĥΓ ' e ⇒ B

5.īĠ

A#M=B

Γ'e⇒A

Γ, Y : A ' e ⇐ B· ' u ⇒ B

Γ ' u , , u  ⇒ A  B

u  ≈ u

A∗B

5"ħħ

Γ'e⇐A

Γ'e:A⇒A

54Įě

Γ'e⇒A

A <: BΓ'e⇐B'JHVSF  #JEJSFDUJPOBM 5ZQJOH %JTKPJOUOFTTϞϞ 5ĲĩĞ 4ĨĮħĝħĞĬĬ Ěħĝ %ĞĭĞīĦĢħĢĬĦ
"MM QSPQFSUJFT JODMVEJOH TVCKFDU SFEVDUJPO BOE UZQF TPVOEOFTT TIPXO JO UIF êSTU DBMDVMVTBMTP IPME JO UIJT DBMDVMVT 8F POMZ GPDVT PO EFUFSNJOJTN IFSF XIJDI JT UIF NPTU JOUFSFTUJOHQSPQFSUZ PG UIF DBMDVMVT XJUI EJTKPJOUOFTT-FNNB  %FUFSNJOJTN PG $BTUJOH  *G · ' v ⇒ A v )−→B v1 BOE v )−→B v2 UIFO
v1 = v2 -FNNB  %FUFSNJOJTN "QQMJDBUJPOT BOE 1SPKFDUJPOT 
t *G · ' v1 v2 ⇒ A v1 • v2 "→ e1 BOE v1 • v2 "→ e2 UIFO e1 = e2 t *G · ' v.l ⇒ A v • l "→ e1 BOE v • l "→ e2 UIFO e1 = e2 ćFPSFN  %FUFSNJOJTN  *G · ' e ⇔ A e )−→ e1 BOE e )−→ e2 UIFO e1 = e2  5ZQF 4PVOEOFTT BOE %FUFSNJOJTN$BTUJOHv )−→A v "$ĭ*ħĭ

$ĭ5Ĩĩ

J : A )−→AMi J : AMiv )−→A 1 : AO

A <: AMi$ĭ"īī

6AO 7¬6Do 7

E <: C → Do

(λY. e : A → B) : E )−→(C→Do ) (λY. e : A → Do ) : (C → Do )$ĭ3Ĝĝ

v )−→AO v "¬6AO 7$ĭ.īĠ3v , , v )−→AO v"v , , v )−→AO v"v )−→AO v"{M = v} )−→{M:AO } {M = v " }$ĭ"ħĝ

$ĭ.īĠ-A " A # Av )−→A v

v )−→AO v"v )−→A vv )−→A v , , v

'JHVSF  $BTUJOH %JTKPJOUOFTT"QQMJDBUJWF %JTQBUDIJOH(v • vl) "→ e"ĩĩ5Ĩĩ-ĢĤĞ"ĩĩ1īĨģ

6A7((p : A) • v) "→ 1 : tail A"ĩĩ-ĚĦ

v )−→A v "({M = v} • M) "→ v
¬6D7((λY. e : A → B) : C → D • v) "→ e[Y )→ v " ] : D"ĩĩ.īĠ-1v2 2 # 1vl2 = .

(v • vl) "→ e(v , , v • vl) "→ e"ĩĩ.īĠ1

1v1 2 # 1vl2 /= .

1v2 2 # 1vl2 /= .

"ĩĩ.īĠ3

1v1 2 # 1vl2 = .

(v • vl) "→ e(v • vl) "→ e(v • vl) "→ e(v , , v • vl) "→ e(v , , v • vl) "→ e , , e

'JHVSF  "QQMJDBUJWF %JTQBUDIJOH %JTKPJOUOFTT " $BMDVMVT XJUI " %JTKPJOU .FSHF 0QFSBUPS

4NBMM4UFQ 3FEVDUJPOe )−→ e"4ĭĞĩ*ħĭ"ħħ

4ĭĞĩ"īī"ħħJ )−→ J : AMi

λY. e : A → B )−→ (λY. e : A → B) : A → B

4ĭĞĩ1į4ĩĥĢĭ

4ĭĞĩ1Ěĩĩ

4ĭĞĩ1ĩīĨģ

4ĭĞĩ7Ěĥ"ħħp : A )−→ p : A , , p : Av v )−→ ev.M )−→ v "v : A )−→ v "A " A # A(v • v ) "→ e4ĭĞĩ"ĩĩ-4ĭĞĩ"ĩĩ3e e )−→ e" ev e )−→ v e"e )−→ e"

e )−→ e"

4ĭĞĩ.īĠ-

4ĭĞĩ.īĠ3e , , v )−→ e" , , vv , , e )−→ v , , e"

e )−→ e"

e )−→ e"

4ĭĞĩ3Ĝĝe )−→ e"{M = e} )−→ {M = e" }(v • M) "→ v "4ĭĞĩ.īĠ1ĚīĚĥĥĞĥ

e )−→ e"

e )−→ e"

e , , e )−→ e" , , e"
4ĭĞĩ"ħħ¬e ∈ pe )−→ e"e : A )−→ e" : A

4ĭĞĩ1īģe )−→ e"e.M )−→ e" .M'JHVSF  0QFSBUJPOBM 4FNBOUJDT %JTKPJOUOFTTv )−→A v "ϟ *ĦĩĥĞĦĞħĭĚĭĢĨħ
ѮJT DIBQUFS HJWFT BO JOUFSQSFUFS JNQMFNFOUBUJPO PG PVS DBMDVMVT JO $IBQUFS  6OMJLF USBEJUJPOBM BQQSPBDIFT PG VTJOH EBUBUZQFT UP SFQSFTFOU UIF UZQFT FYQSFTTJPOT FUD XF UBLF B NPSF
EJSFDU BOE SFMBUJWFMZ TJNQMF SFQSFTFOUBUJPO TZNCPMT "MM UIF BMHPSJUINT BSF DPNQVUFE WJBTZNCPMJD QBUUFSO NBUDIJOH BOE EJTQBUDIJOH ѮJT BQQSPBDI TBWFT VT GSPN XSJUJOH B QBSTFS PG
PVS MBOHVBHFT TJODF XF BEPQU 4FYQSFTTJPOT <.D$BSUIZ > BOE USFBU UIJT JNQMFNFOUBUJPOBT B EJBMFDU PG -JTQ UIPVHI TUBUJDBMMZ UZQFEϟϚ 4ĭĚĭĢĜĬ
8F TUBSU XJUI UIF EFêOJUJPO PG UZQFT BOE UFSNT BOE UIFO JOUSPEVDF UIF TVCUZQJOH BMHPSJUIN*O UIF MBTU QBSU XF JNQMFNFOU UZQF JOGFSFODF BOE UZQF DIFDLJOHϟϚϚ 5ĲĩĞĬ Ěħĝ 5ĞīĦĬ'JSTU XF EFêOF PVS TZOUBY BT TFWFSBM DPOUSBDUT BLB QSFEJDBUFT  'PS ivT2\ XF IBWF CBTJDUZQFT JOUFHFS ëPBUJOH OVNCFS CPPMFBO UPQ BOE DPNQPVOE UZQFT GVODUJPO UZQFT JOUFSTFDUJPO UZQFT BOE SFDPSE UZQFT  'PS TJNQMJDJUZ UIF MBCFM JT KVTU JOUFSQSFUFE BT B OVNCFS
U/27BM2 H#2H\ MmK#2`\V
U/27BM2 UivT2\ iV
UKi+? i(^BMi(^7HQi(^#QQH(^iQT(<U→ -U\ ivT2\V -U\ ivT2\VV(<U -U\ ivT2\V -U\ ivT2\VV(<U -U\ H#2H\V -U\ ivT2\VV
(n

Oi)
Oi)
Oi)
Oi)
Oi)
Oi)
Oi)
O7)VV

'PS UFSNT XF IBWF WBSJBCMFT OVNCFST CPPMFBOT MBNCEB BCTUSBDUJPOT GVODUJPO BQQMJDBUJPOTNFSHFT FH UK 2R 2kV BOOPUBUFE UFSNT SFDPSET FH U= H 2V BOE SFDPSE QSPKFDUJPOTFH UI 2 HV BOE QSJNJUJWF BEEJUJPOT FH BMiY- 7HQY  *NQMFNFOUBUJPO
U/27BM2 U2tT`\ 2V
UKi+? 2(U\ bvK#QH\V(U\ 2t+i@BMi2;2`\V(U\ 7HQMmK\V
(^Oi
(^O7
(<Uλ U-U\ bvK#QH\V , -U\ ivT2\VV -U\ 2tT`\V -U\ ivT2\VV(<U-U\ 2tT`\V -U\ 2tT`\VV(<UK -U\ 2tT`\V -U\ 2tT`\VV(<U, -U\ 2tT`\V -U\ ivT2\VV(<U= -U\ H#2H\V -U\ 2tT`\VV(<UI -U\ 2tT`\V -U\ H#2H\VV(<UBMiY -U\ 2tT`\V -U\ 2tT`\VV(<U7HQY -U\ 2tT`\V -U\ 2tT`\VV
(n

Oi)
Oi)
Oi)
Oi)
Oi)
Oi)
Oi)
Oi)
Oi)
Oi)
Oi)
Oi)
Oi)
O7)VV

ϟϚϛ 4ĮěĭĲĩĢħĠ
"ѫFS UIF TZOUBY JT TFUUMFE XF OPX EFêOF PVS TVCUZQJOH BOE BQQMJDBUJWF TVCUZQJOH BMHPSJUINT
8F êSTU EFêOF UIF PSEJOBSZ KVEHNFOU BT B DPOUSBDU BOE MFU TQMJUUBCMF UZQFT CF B GVODUJPO UIBUBDDFQUT B UZQF BOE SFUVSOT B QBJS PG UZQFT ѮF DPOUSBDU PG UIF TQMJU GVODUJPO EFTDSJCFT UIBU JU
BDDFQUT B OPOPSEJOBSZ UZQF BOE SFUVSOT UXP UZQFT
U/27BM2f+QMi`+i UQ`/\ iV
U→ ivT2\ #QQH2M\VUKi+? i(^BMi(^7HQi(^#QQH(^iQT(<U→ -n -"V(<U -n -V
(n

Oi)
Oi)
Oi)
Oi)
UQ`/\ "V)UQ`/\ V)
O7)VV

U/27BM2f+QMi`+i UbTH iVU→ UM/f+ ivT2\ UMQif+ Q`/\VV U+QMbf+ ivT2\ ivT2\VV
UKi+? i(<U→ - -"V
UH2i U("b UbTH "V)V
<UU→ - -U+` "bVV X U→ - -U+/` "bVVVV)(<U -H -V
UH2i U(b UbTH V)V 4UBUJDT<UU-H -U+` bVV X U(<U - -"V(n-H -U+/` bVVVV)<U- X -"V)U2``Q` ]7BH iQ bTHBi] iV)VVѮF TVCUZQJOH SFMBUJPO JT NPEFMMFE BT B GVODUJPO UIBU UBLFT UXP UZQFT BT JOQVUT BOE SFUVSOT B
CPPMFBO TQFDJGZJOH JG UXP UZQFT IBWF UIF TVCUZQJOH SFMBUJPO ѮF êSTU GPVS CSBODIFT EFBM XJUICBTJD UZQFT BOE UPQ UZQFT 'PS DPNQPVOE UZQFT XF DIFDL XIFUIFS UIFZ BSF PSEJOBSZ UZQFTBOE UIFO EJTQBUDI UIFN JOUP EJĒFSFOU PQUJPOT 4JNQMZ TQFBLJOH XF LFFQ TQMJUUJOH UZQFT POUIF SJHIU TJEF VOUJM UIFZ BSF PSEJOBSZ UIFO XF BQQMZ SVMFT GPS BSSPXT BOE SFDPSET UP UIFN
U/27BM2f+QMi`+i Ubm#\ iR ikV
U→ ivT2\ ivT2\ #QQH2M\VUKi+? UiR ikV(U^BMi ^BMiV
Oi)(U^7HQi ^7HQiV
Oi)(U^#QQH ^#QQHVOi)Oi)(Un ^iQTV(U<U→ - -"V <U→ -* -U\ Q`/\ .VVVUM/ Ubm#\ * V Ubm#\ " .VV)(U<U -H -V <U -H -U\ Q`/\ "VVV
Ubm#\  "V)(U U\ UMQif+ Q`/\V "VV UH2i U("b UbTH "V)V
UM/ Ubm#\  U+` "bVV Ubm#\  U+/` "bVVVV)(U<U - -"V U\ Q`/\ *VV
UQ` Ubm#\  *V Ubm#\ " *VV)
(Un nVO7)VVϟϚϜ "ĩĩĥĢĜĚĭĢįĞ 4ĮěĭĲĢĩħĠ
0VS TFMFDUPS UZQFT BSF UZQFT PS MBCFMT BOE XF EFêOF UIFN CZ DPNCJOJOH DPOUSBDUT ivT2b\
BOE H#2H\ 'PS PVUQVU UZQFT UP EFOPUF UIF TVDDFTT PS GBJMVSF XF DPNCJOF ivT2\ BOE 7BH\
ѮFSF JT POMZ POF JOIBCJUBOU O7 GPS UIF DPOUSBDU 7BH\
ѮF DPNQPTJUJPO PQFSBUPS JT TJNQMZ JNQMFNFOUFE BT B GVODUJPO UIBU UBLFT UXP PVUQVUT BOE
SFUVSOT BO PVUQVU UZQF bm# JT UIF GVODUJPO GPS BQQMJDBUJWF TVCUZQJOH JU UBLFT B SFHVMBS UZQF
BOE B TFMFDUPS UZQF UIFO SFUVSOT UIF SFTVMU UZQF JG TVDDFTT PUIFSXJTF JU SFUVSOT O7 BT B GBJMVSF
U/27BM2 b2H2+iQ`\ UQ`f+ ivT2\ H#2H\VV
U/27BM2 U7BH\ iV U2[mH\ i O7VV
U/27BM2 QmiTmi\ UQ`f+ ivT2\ 7BH\VV
U/27BM2f+QMi`+i U+QK# QR QkVU→ QmiTmi\ QmiTmi\ QmiTmi\VUKi+? UQR QkV(UU\ ivT2\ RV U\ ivT2\ kVV

<U -R -kV) *NQMFNFOUBUJPO(UU\ 7BH\V U\ ivT2\ VV(UU\ ivT2\ V U\ 7BH\VV(UU\ 7BH\V U\ 7BH\VV

)
)
O7)VV

U/27BM2f+QMi`+i Ubm# i bV
U→ ivT2\ b2H2+iQ`\ QmiTmi\VUKi+? Ui bV(U<U→ -R -kV U\ ivT2\ "VV O,r?2M Ubm#\ " RVk)(U<U→ -R -kV U\ ivT2\ "VV
O7)(U<U -HR -V U\ H#2H\ HkVV O,r?2M U2[mH\ HR HkV)(U<U -HR -V U\ H#2H\ HkVV
O7)
(U<U -R -kV aV
U+QK# Ubm# R aV Ubm# k aVV)
(Un nVO7)VVϟϚϝ 5ĲĩĢħĠѮF CJEJSFDUJPOBM UZQJOH JT JNQMFNFOUFE BT UXP GVODUJPOT BM72` BOE +?2+F ѮF GVODUJPO
BM72` UBLFT B UFSN BOE BO FOWJSPONFOU BT JOQVUT BOE SFUVSOT B UZQF BT BO PVUQVU ѮBU JT UPTBZ UIF UZQF PG JU JT U→ 2tT`\ HBbi\ ivT2\V ѮF GVODUJPO +?2+F UBLFT UISFF BSHVNFOUT B
UFSN B WBSJBCMF FOWJSPONFOU BOE B UZQF UIBU OFFET UP CF DIFDLFE *U SFUVSOT B CPPMFBO WBMVFTQFDJGZJOH XIFUIFS UIF DIFDL TVDDFTTU/27BM2f+QMi`+i U+?2+F 2 i 2MpV
U→ 2tT`\ ivT2\ HBbi\ #QQH2M\VUH2i U( UBM72` 2 2MpV)V Ubm#\  iVVV
U/27BM2f+QMi`+i UBM72` 2 2MpV
U→ 2tT`\ HBbi\ ivT2\VUKi+? 2(U\ 2t+i@BMi2;2`\V^BMi)(U\ 7HQMmK\V^7HQi)(^Oi^#QQH)(^O7^#QQH)(U\ bvK#QH\V
UHQQFmT 2Mp 2V)(<Uλ U-t , -V -2 -"V O,r?2M U+?2+F 2 " U+QMb <U-t -V 2MpVV<U→ - -"V)(<U= -H -2V<U -H -UBM72` 2 2MpVV)(<U, -2 -V O,r?2M U+?2+F 2  2MpV)(<U-2R -2kV
UH2i U( UBM72` 2R 2MpV) (" UBM72` 2k 2MpV)V
UQ` Ubm#  "V U2``Q` ]TT]VVV)(<UI -2 -HVUH2i U( UBM72` 2 2MpV)V
UQ` Ubm#  HV U2``Q` ]T`QD]VVV) %ZOBNJDT(<UK -2R -2kV

UH2i U( UBM72` 2R 2MpV) (" UBM72` 2k 2MpV)V<U - -"VV)(<UBMiY -2R -2kV O,r?2M UM/ U+?2+F 2R ^BMi 2MpV
U+?2+F 2k ^BMi 2MpVV^BMi)(<U7HQY -2R -2kV O,r?2M UM/ U+?2+F 2R ^7HQi 2MpV
U+?2+F 2k ^7HQi 2MpVV^7HQi)(n
U2``Q` ]+MMQi BM72` i?2 ivT2 Q7] 2 ]mM/2`] 2MpV)VVϟϛ %ĲħĚĦĢĜĬ'PS UIF EZOBNJD TFNBOUJDT XF êSTU EFêOF UXP DPOUSBDUT SBX WBMVF BOE WBMVF ѮFO XF TQFDJGZ UIBU B DBTUJOH GVODUJPO BDDFQUT B WBMVF BOE B UZQF JU SFUVSOT UIF SFTVMU WBMVF JG TVDDFTTGVM
PUIFSXJTF JU GBJMT ѮF GVODUJPO /BbT JNQMFNFOUT PVS BQQMJDBUJWF EJTQBUDIJOH JU BDDFQUT B
WBMVF BOE B TFMFDUPS BOE SFUVSOT BO FYQSFTTJPOU/27BM2f+QMi`+i UTpHm2\ 2V XXXV
U/27BM2f+QMi`+i UpHm2\ 2V XXXV
U/27BM2f+QMi`+i U+bi 2 iVU→ pHm2\ ivT2\ UQ`f+ pHm2\ 7BH\VV
UKi+? U2 iV(U<U, -M -V ^BMiV O,r?2M Ubm#\  ^BMiV<U, -M BMiV)(U<U, -M -V ^7HQiV O,r?2M Ubm#\  ^7HQiV<U, -M 7HQiV)(U<U, Oi -V ^#QQHV O,r?2M Ubm#\  ^#QQHV^U, Oi #QQHV)(U<U, O7 -V ^#QQHV O,r?2M Ubm#\  ^#QQHV^U, O7 #QQHV)(Up ^iQTV^U, R iQTV)(U<U, Uλ U-t , -V -2 -"V -1V <U→ -* -U\ Q`/\ .VVVO,r?2M Ubm#\ 1 <U→ -* -.VV<U, Uλ U-t , -V -2 -.V U→ -* -.VV)(U<U= -H -pV <U -H -U\ Q`/\ VVV
<U= -H -U+bi p VV)
(U<UK -pR -pkV U\ Q`/\ VV O,r?2M U+bi pR V
U+bi pR V)(U<UK -pR -pkV U\ Q`/\ VV O,r?2M U+bi pk V
U+bi pk V)(Up U\ UMQif+ Q`/\V VV
UH2i U(b UbTHBi V)V <UK -U+bi p U+` bVV -U+bi p U+/` bVVVV)(Un nV
O7)VV
U/27BM2f+QMi`+i U/BbT p pHV
U→ pHm2\ UQ`f+ H#2H\ pHm2\V 2tT`\V
UKi+? p(<U, Uλ U-t , -V -2 -"V U→ -* -.VV<U, -Ubm#bi 2 t U+bi pH VV -.V)(<U= -H -pV O,r?2M U2[mH\ H pHVp) *NQMFNFOUBUJPO(<UK -pR -pkV O,r?2M UMQi Ubm# UTi pkV Ui pHVVV
U/BbT pR pHV)(<UK -pR -pkV O,r?2M UMQi Ubm# UTi pRV Ui pHVVV
U/BbT pk pHV)(<UK -pR -pkV O,r?2M UM/ Ubm# UTi pRV Ui pHVV
Ubm# UTi pkV Ui pHVVV<UK -U/BbT pR pHV -U/BbT pk pHVV)VV

5P FWBMVBUF UIF UFSN XF DIPPTF UIF TNBMMTUFQ BQQSPBDI 'JSTU XF EFWFMPQ B bi2T GVODUJPO XIJDI NPEFMT PVS PQFSBUJPOBM TFNBOUJDT ѮFO UIF 2pH GVODUJPO FWBMVBUFT UIF UFSNTNVMUJQMF UJNFT VOUJM UIFZ IBWF B DBOPOJDBM GPSN
U/27BM2f+QMi`+i Ubi2T 2V
U→ 2tT`\ 2tT`\V
UKi+? 2(U\ 2t+i@BMi2;2`\ MV<U, -M BMiV)(U\ 7HQMmK\ MV<U, -M 7HQiV)(^Oi^U, Oi #QQHV)(^O7^U, O7 #QQHV)(<Uλ U-t , -V -2 -"V<U, Uλ U-t , -V -2 -"V U→ - -"VV)(<U, -U\ TpHm2\ TV -U\ UMQif+ Q`/\V VV
UH2i U(b UbTH V)V
<UK U, -T -U+` bVV U, -T -U+/` bVVVV)(<UI -U\ pHm2\ pV -U\ H#2H\ HVV
U/BbT p HV)(<UI -U\ UMQif+ pHm2\V 2V -U\ H#2H\ HVV<UI -Ubi2T 2V -HV)(<U= -U\ H#2H\ HV -U\ UMQif+ pHm2\V 2VV<U= -H -Ubi2T 2VV)(<U-U\ pHm2\ pV -U\ pHm2\ pHVV
U/BbT p pHV)(<U, -U\ pHm2\ pV -V
U+bi p V)(<U, -U\ UMQif+ TpHm2\V 2V -V<U, -Ubi2T 2V -V)(<U-U\ UMQif+ pHm2\V 2RV -2kV
<U-Ubi2T 2RV -2kV)(<U-U\ pHm2\ pV -2kV
<U-p -Ubi2T 2kVV)(<UK -2R -U\ pHm2\ pVV<UK -Ubi2T 2RV -pV)(<UK -U\ pHm2\ pV -2kV
<UK -p -Ubi2T 2kVV)(<UK -2R -2kV
<UK -Ubi2T 2RV -Ubi2T 2kVV)(<UBMiY -U\ UMQif+ pHm2\V 2RV -2kV
<UBMiY -Ubi2T 2RV -2kV)(<UBMiY -U\ pHm2\ pV -U\ UMQif+ pHm2\V 2kVV <UBMiY -p -Ubi2T 2kVV)(<UBMiY -U\ pHm2\ pRV -U\ pHm2\ pkVV
UTHmb pR pkV)(<U7HQY -U\ UMQif+ pHm2\V 2RV -2kV<U7HQY -Ubi2T 2RV -2kV)(<U7HQY -U\ pHm2\ pV -U\ UMQif+ pHm2\V 2kVV <U7HQY -p -Ubi2T 2kVV)(<U7HQY -U\ pHm2\ pRV -U\ pHm2\ pkVV
UTHmb pR pkV)VV
U/27BM2f+QMi`+i U2pH 2V
U→ Mvf+ pHm2\V
UH2i U(2 U/2bm;` 2V)V
Ur?2M UBM72` 2 ^UVV UB7 UpHm2\ 2V 2 U2pH Ubi2T 2VVVVVV 5PVSϟϜ 5ĨĮī
ѮJT TFDUJPO HJWFT B UPVS PG PVS MBOHVBHF BOE FBDI MJOF JT EPDVNFOUFE JO UIF DPNNFOUT
cc bBKTH2 HBi2`H
9k 9kXk Oi O7
cc λ #bi`+iBQM
Uλ Ut , BMiV t BMiV
cc 7mM+iBQM TTHB+iBQM
UUλ Ut , BMiV t BMiV RV
cc `2+Q`/ +`2iBQM- 7Q` bBKTHB+Biv- r2 mb2 MmK#2`b iQ `2T`2b2Mi i?2 H#2H
U= 9k OiV
cc `2+Q`/ T`QD2+iBQM
UI U= 9k OiV
9kV
cc K2`;2 irQ pHm2b
UK R OiV
cc K2`;2 irQ 7mM+iBQMb
UK Uλ Ut , BMiV t BMiVUλ Ut , #QQHV t #QQHVV
cc K2`;2/ 7mM+iBQM +M #2 TTHB2/UUK Uλ Ut , BMiV t BMiVUλ Ut , #QQHV t #QQHVV
RV
cc K2`;2 irQ `2+Q`/b
UK U= R OiVU= k O7VV
cc K2`;2/ `2+Q`/b +M #2 b2H2+i2/ #v H#2H
UI UK U= R OiVU= k O7VV
RV
cc K2`;2/ `;mK2Mib +M HbQ #2 miQKiB+HHv b2H2+i2/ *NQMFNFOUBUJPOUUλ Ut , BMiV t BMiVUK R OiVV
cc M 2tT`2bbBQM +M #2 MMQii2/
U, Uλ Ut , BMiV t BMiVU→ BMi BMiVV
cc MMQii2  ]pHm2] +M 7Q`+2  /QrM+bifmT+bi
U, U, R BMiVU BMi BMiVV cc ⇒ /mTHB+i2  MmK#2`
U, U, Uλ Ut , BMiV t BMiV U→ BMi BMiVVU U→ BMi BMiVU→ BMi BMiVVV cc ⇒ /mTHB+i2  7mM+iBQM
U, UK Uλ Ut , BMiV t BMiVUλ Ut , #QQHV t #QQHVVU→ #QQH #QQHVV cc ⇒ /QrM+bi iQ  #QQH2M B/2MiBiv 7mM+iBQM
cc mb2 BMiY iQ // BMi2;2`b
UBMiY R jV
cc mb2 7HQY iQ // 7HQib
U7HQY RXy kXRVUUλ Ut , BMiV UBMiY t tV BMiV RVUUλ Ut , 7HQiV U7HQY t tV 7HQiV RXRV
cc Qp2`HQ/ BMiY M/ 7HQY iQ +`2i2  TQHvKQ`T?B+ ]/Qm#H2] 7mM+iBQM
UUK Uλ Ut , BMiV UBMiY t tV BMiVUλ Ut , 7HQiV U7HQY t tV 7HQiVV
RV
cc p`B/B+ p2`bBQM Q7 K2`;2 QT2`iQ`
UI UJ U= R OiVU= k O7V
U= j OiVVkV
cc MQi?2` bvMi+iB+ bm;` 7Q` `2+Q`/b
U_ UR OiV U9j O7V UNN OiVVϠ 3ĞĥĚĭĞĝ 8ĨīĤϠϚ *ħĭĞīĬĞĜĭĢĨħ 5ĲĩĞĬ .ĞīĠĞĬ Ěħĝ 0įĞīĥĨĚĝĢħĠ
'PSTZUIF JOUSPEVDFE CZ 3FZOPMET <> IBT B SFTUSJDUFE NFSHF PQFSBUPS BOE JUT DPIFSFOU
TFNBOUJDT JT GPSNBMMZ QSPWFO )PXFWFS JU EPFT OPU BDDPVOU GPS PWFSMPBEFE GVODUJPOT TJODF
NVMUJQMF GVODUJPOT BSF GPSCJEEFO CZ NFSHFT 1JFSDF <> JOUSPEVDFE B ;Hm2 DPOTUSVDU JOIJT DBMDVMVT F∧ BT B MBOHVBHF FYUFOTJPO UP TVQQPSU VTFSEFêOFE PWFSMPBEJOH BOE UIF UZQFT

PG PWFSMPBEFE GVODUJPOT BSF BMTP NPEFMMFE BT JOUFSTFDUJPO UZQFT )PXFWFS UIF NFUBUIFPSZ PG
UIF HMVF PQFSBUPS IBT OPU CFFO TUVEJFE%JSFDUMZ DPNQVUJOH UIF UZQF XJUI BSHVNFOUT BOE GVODUJPOT JO UIF BQQMJDBUJPO SVMF JT OPU
OFX 0SJHJOBMMZ JU BQQFBST BT UIF GVODUJPO BQQUZQF JO UIF XPSL PG 'SFFNBO BOE 1GFOOJOH<> ѮF JEFB PG BQQUZQF JT TJNQMF JG UIF GVODUJPO IBT UIF UZQF (A1 → B1 )  (A2 →B2 )  ...  (An → Bn ) BOE UIF BSHVNFOU IBT UIF UZQF A UIF SFTVMU UZQF XJMM CF EFSJWFE
Bi
i|A≤Ai
ѮF BMHPSJUIN JT CBTFE PO UIF SFêOFNFOU UZQFT XIJDI BSF SFXSJUUFO JOUP VOJPO OPSNBM GPSN
BOE JOUFSTFDUJPO OPSNBM GPSN XIFSF UIF EJTUSJCVUJWJUZ PG JOUFSTFDUJPO UZQFT XJMM OPU BQQFBS"MTP UIF BQQUZQF BMHPSJUIN JT JOUFHSBUFE JOUP B UZQF JOGFSFODF BMHPSJUIN UIF DPSSFDUOFTTPG UIF BMHPSJUIN JT JNQMJFE CZ UIF DPSSFDUOFTT PG UIF JOGFSFODF BOE DPSSFTQPOEJOH EZOBNJDTFNBOUJDT JT OPU EFTJHOFE
%VOêFMET DBMDVMVT <%VOêFME > JT QPXFSGVM FOPVHI UP FODPEF PWFSMPBEFE GVODUJPOTBOE SFDPSE QSPKFDUJPO 6OMJLF PVS DBMDVMJ JU EPFT OPU TVQQPSU EJTUSJCVUJWJUZ BOE OFTUFE DPNQPTJUJPO ѮJT NFBOT UIBU PWFSMPBEFE GVODUJPOT EP OPU JOUFSBDU OJDFMZ XJUI DVSSZJOH 'PS FYBNQMF UP QSPHSBN Tb?Qr mMBi R JO IFS DBMDVMVT XF TIPVME XSJUF UUTb?Qr mMBiV , AMi →"QQHV R "T BDLOPXMFEHFE CZ %VOêFME UIF TFNBOUJDT JT OPU EFUFSNJOJTUJD ѮJT JT TJNJMBSUP PVS êSTU DBMDVMVT JO $IBQUFS  5P SFTUSJDU UIF QPXFS PG UIF NFSHF PQFSBUPS BOE FOBCMF
EFUFSNJOJTN B EJTKPJOUOFTT SFTUSJDUJPO PO NFSHFT IBT CFFO QSPQPTFE <0MJWFJSB FU BM >
$MPTFTU UP PVS XPSL JT UIF λ+i DBMDVMVT <)VBOH FU BM > XIJDI JT B EFUFSNJOJTUJD DBMDVMVTXJUI JOUFSTFDUJPO UZQFT BOE B EJTKPJOU NFSHF PQFSBUPS ѮFSF BSF UXP NBKPS EJĒFSFODFT CF 3FMBUFE 8PSLUXFFO PVS XPSL BOE λ+i   0VS êSTU DBMDVMVT VUJMJ[FT BO VOSFTUSJDUFE NFSHF PQFSBUPS XIJDIBMMPXT BOZ GVODUJPOT BOE SFDPSET UP CF NFSHFE  0VS TFDPOE DBMDVMVT DBO CF WJFXFE BT
B WBSJBOU PG λ+i UIBU FNQMPZT BQQMJDBUJWF TVCUZQJOH BOE UIVT BWPJET NBOZ VOOFDFTTBSZ BOOPUBUJPOT UIBU BSF SFRVJSFE JO λ+i TJODF GVODUJPO PWFSMPBEJOH BOE SFDPSE QSPKFDUJPO BSF OPU+
EJSFDUMZ TVQQPSUFE JO λ+i  *O λi XF XPVME OFFE B UFSN XJUI BO FYQMJDJU UZQF BOOPUBUJPO JOTUFBE UUbm++--MQiV , AMi → AMiV R ѮF SJHJE GPSN PG BQQMJDBUJPOT BOE QSPKFDUJPOT JO+λ+i QSFWFOUT FYQSFTTJPOT TVDI BT Ubm++--MQiV R XIJDI BSF OPU XFMMUZQFE JO λi 

*O SFDFOU XPSL <3JPVY FU BM > QSPQPTFE B DBMDVMVT XJUI B EJTKPJOU NFSHF PQFSBUPS UIBUEFBMT XJUI VOJPO UZQFT BOE PWFSMPBEJOH ѮJT JT BDIJFWFE XJUI UXP NPSF êOFHSBJOFE EJTKPJOUOFTT SFMBUJPOT DBMMFE NFSHFBCJMJUZ BOE EJTUJOHVJTIBCJMJUZ 4JNJMBSMZ UP PVS DBMDVMVT UIFZDPOTJEFS BO FYQSFTTJWF UZQFMFWFM EJTQBUDI SFMBUJPO UIBU QMBZT UIF TBNF SPMF BT BQQMJDBUJWF TVCUZQJOH JO PVS DBMDVMVT 4VDI EJTQBUDIJOH SFMBUJPO TVQQPSUT VOJPO UZQFT VOMJLF PVS DBMDVMVT*O UFSNT PG UIF PQFSBUJPOBM TFNBOUJDT UIFSF BSF TJHOJêDBOU EJĒFSFODFT CFUXFFO PVS XPSL BOE
3JPVY FU BMT XPSL 8IJMF UIFJS TFNBOUJDT TUJMM FNQMPZT UZQFT BU SVOUJNF UIFSF JT OP DBTUJOHSFMBUJPO *OTUFBE UIFSF BSF QBUUFSOT BOE DPQBUUFSOT XIJDI FOGPSDF SVOUJNF DPFSDJPOT WJBηFYQBOTJPO 8IJMF PWFSMPBEJOH JT TVQQPSUFE UIF EJTKPJOUOFTT SFMBUJPOT BSF TUJMM OPU ëFYJCMF
FOPVHI UP TVQQPSU SFUVSO UZQF PWFSMPBEJOHϠϛ λó$ĚĥĜĮĥĮĬ
$BTUBHOB FU BM <> HBWF B GPSNBMJTBUJPO UP DBMDVMVT GPS PWFSMPBEFE GVODUJPOT XJUI TVCUZQ
JOH *O IJT DBMDVMVT PWFSMPBEFE GVODUJPOT BSF EFêOFE BT UFSNT BOE UIFJS BQQMJDBUJPO JT
TQFDJBMMZ USFBUFE BT B OFX BQQMJDBUJPO UFSN TJODF UIFZ BEPQU UXP EJĒFSFOU NFDIBOJTNT ѮF
TZOUBY PG IJT DBMDVMVT JT EFêOFE BT GPMMPXT ѮF NPTU JOUFSFTUJOH QBSU JT IJHIMJHIUFE XIFSF
M V M JT VTFE GPS BEEJOH OFX JOTUBODFT GPS PWFSMPBEFE GVODUJPOT BOE M • M JT VTFE GPS
PWFSMPBEFE BQQMJDBUJPOT

5FSNT M ::= xV | λxV . M | M · M | $ | M V M | M • M
ѮF UZQFT PG PWFSMPBEFE GVODUJPOT BSF B êOJUF MJTU PG BSSPX UZQFT XJUI B DPOTJTUFODZ SFTUSJDUJPO
1SF5ZQFT V ::= A | V → V | {V1" → V1"" , ..., Vn" → Vn"" } 5ZQF $MBTTFT'PS UZQJOH SVMFT UIF OFX JOUSPEVDUJPO SVMF BOE FMJNJOBUJPO SVMF BSF BEEFE\^*ħĭīĨ

\^&ĥĢĦ

' M : W1 ≤ {Ui → Vi }i≤(n−1)' N : W2 ≤ U n → Vn

' (M {Ui →Vi }i≤n N ) : {Ui → Vi }i≤n

' M : {Ui → Vi }i∈I

'N :U

Uj = mini∈I {Ui |U ≤ Ui }' M • N : Vj

6OMJLF PVS TUSBUFHZ BMM UIF êUUJOH CSBODIFT XJMM CF BDDFQUFE PS SFKFDUFE XIFO BNCJHVJUJFTBSF EFUFDUFE ѮJT UZQJOH SVMF XJMM JOGFS UIF SFTVMU UZQF PG UIF iCFTUNBUDIu CSBODI BOE BQQMZUIBU CSBODI BU SVOUJNF ѮF TFNBOUJDT JT UZQFEFQFOEFOU BOE PWFSMPBEFE BQQMJDBUJPOT SFMZPO UIF SVOUJNF UZQFT XIJDI JT TJNJMBS UP PVS 5%04 BQQSPBDI
ѮF DPOëVFODF BOE TVCKFDUSFEVDUJPO BSF QSPWFE JO IJT DBMDVMVT %JĒFSFOUMZ UP PVS BQQSPBDI UIF OFTUFE DPNQPTJUJPO JT OPU TVQQPSUFE JO IJT DBMDVMVT .PSFPWFS POMZ POF CSBODIDBO CF TFMFDUFE JO UIF PWFSMPBEFE BQQMJDBUJPO UIVT UFSNT MJLF bm++--BMihQ.B;Bi BSF SFKFDUFEGPSCJEEJOH DVSSZJOH PO PWFSMPBEFE GVODUJPOT *O IJT XPSL SFDPSET BSF FODPEFE CZ MBNCEBGVODUJPOT BOE NVMUJêFME SFDPSET BSF PWFSMPBEFE GVODUJPOTϠϜ 5ĲĩĞ $ĥĚĬĬĞĬ
5ZQF DMBTTFT <8BEMFS BOE #MPUU > FOBCMF BEIPD QPMZNPSQIJTN CZ BEEJOH DPOTUSBJOUT UP
QPMZNPSQIJD UZQFT XIJDI JT DPNQMFUFMZ EJĒFSFOU GSPN PVS BQQSPBDI ѮF UZQF TJHOBUVSF PG
PWFSMPBEFE GVODUJPOT JT EFêOFE JO B DMBTT XIJDI JT BO JOUFSGBDF UIBU TUBUFT UIF UZQFT PG PWFSMPBEFE GVODUJPOT 8F DBO TJNQMZ BEE UIF JNQMFNFOUBUJPO PG PWFSMPBEFE GVODUJPOT CZ XSJUJOH
JOTUBODFT ѮF PWFSMPBEFE BQQMJDBUJPO XJMM CF NBEF CZ JOTUBODF SFTPMVUJPO ѮF FYQSFTTJWF
OFTT PG UZQF DMBTTFT JT NPSF QPXFSGVM UIBO PVS BQQSPBDI 'PS FYBNQMF
b?Qr ,, a?Qr  ⇒  → ai`BM;b?Qr (R-k) @@ 2pHmi2/ iQ ](R-k)]*U BMTP XPSLT êOF XJUI UIF DVSSJFE PWFSMPBEJOH 'PS FYBNQMF BEEJUJPO DBO CF EFêOFE BT 
+Hbb //#H2  # + r?2`2
// ,,  → # → +&BDI JOTUBODF XJMM DSFBUF BO JOTUBODF PG PWFSMPBEFE GVODUJPO //
BMbiM+2 //#H2 AMi AMi AMi r?2`2
// t v 4 t Y v

XJUI .VMUJ1BSBN5ZQF$MBTTFT 'MFYJCMF$POUFYUT FYUFOTJPOT 3FMBUFE 8PSL
BMbiM+2 //#H2 AMi "QQH AMi r?2`2
// t v 4 B7 v i?2M t Y R 2Hb2 t+m``B2/ ,, //#H2 AMi # + ⇒ # → ++m``B2/ 4 // UR ,, AMiV

0OF PG UIF JOUFSFTUJOH XBZT UP DPNQBSF UZQF DMBTTFT XJUI PVS BQQSPBDI JT OFTUFE DPNQPTJUJPO'PS FYBNQMF JG XF BCTUSBDU b?Qr GVODUJPO JO B UIVOL UIF DMBTT a?Qr XJMM BQQFBS BU UIF NPTU
MFѫ *O UIF WJFX PG UIF EJTUSJCVUJWJUZ UIF SFTVMU Tb?Qr UV BOE Tb?Qr UV R JMMVTUSBUF UIBU UIFDMBTT a?Qr DBO EJTUSJCVUF PWFS UIF FBDI JOTUBODF PG Tb?Qr
Tb?Qr ,, a?Qr  ⇒ T →  → ai`BM;
Tb?Qr 4 $t → b?Qr

"OPUIFS QPJOU UP CF OPUFE JT UIBU DPOTUSBJOFE CZ UIF ). UZQF TZTUFN UZQF DMBTTFT JO )BTLFMM
EP OPU TVQQPSU TVCUZQJOHϠϝ 4ĞĦĚħĭĢĜ 4ĮěĭĲĩĢħĠ
4FNBOUJD TVCUZQJOH <'SJTDI FU BM > UBLFT B EJĒFSFOU EJSFDUJPO UP UZQF PWFSMPBEFE GVODUJPOT XJUI JOUFSTFDUJPO UZQFT BOE VOJPO UZQFT *O TFNBOUJD TVCUZQJOH UIF TFNBOUJDT PG UZQFT
JT TFUUIFPSFUJD BOE UIFO TVCUZQJOH SFMBUJPOT BSF EFSJWFE GSPN UIF TFNBOUJDT ѮF UZQF TZTUFN GFBUVSFT JOUFSTFDUJPO UZQFT VOJPO UZQFT BOE OFHBUJPO UZQFT 0WFSMPBEFE GVODUJPOT DBO
CF EFêOFE CZ B UZQFDBTF QSJNJUJWF XIJDI JT TJNJMBS UP UIF FMJNJOBUJPO PG VOJPO UZQFT 'PS
FYBNQMF UIF UZQF PG b?Qr JT AMi | "QQH → ai`BM;ѮF UZQJOH GPS BQQMJDBUJPO JT TUBOEBSE JO UIFJS DBMDVMJ <$BTUBHOB FU BM > BOE EJĒFSFOU

JNQMFNFOUBUJPOT BSF EJTQBUDIFE CZ UIF FYQMJDJU UZQF HJWFO CZ UIF QSPHSBNNFS 'PS FYBNQMF
UIF GVODUJPO b?Qr JT EFêOFE BT
H2i b?Qr 4 7mM t → B7 t Bb AMi i?2M b?QrAMi t 2Hb2 b?Qr"QQH t"MTP bm++--MQi IBT UIF UZQF UAMi → AMiV  U"QQH → "QQHV
H2i bm++MQi 4 7mM t → B7 t Bb AMi i?2M bm++ t 2Hb2 MQi t

ѮF BQQSPBDI UP TFNBOUJD TVCUZQJOH PG PWFSMPBEFE GVODUJPOT JT EJĒFSFOU GSPN PVST TJODF JOPVS DBMDVMJ
r POMZ JOUFSTFDUJPO UZQFT BSF VTFE UP SFQSFTFOU UZQFT PG PWFSMPBEFE GVODUJPOT BOEr PWFSMPBEFE GVODUJPOT DBO CF JOUSPEVDFE CZ TJNQMZ NFSHJOH

 .VMUJNFUIPET BOE .VMUJQMF %JTQBUDIJOH

ϠϞ .ĮĥĭĢĦĞĭġĨĝĬ Ěħĝ .ĮĥĭĢĩĥĞ %ĢĬĩĚĭĜġĢħĠ
$BMDVMJ XJUI TVCUZQJOH FH 'FBUIFSXFJHIU +BWB <*HBSBTIJ FU BM > PѫFO GFBUVSF EJTQBUDIJOH TJODF UZQFT PG UFSNT XJMM CFDPNF NPSF QSFDJTF EVSJOH UIF SFEVDUJPO ѮF GVODUJPO DBMM XJMM
CF SFTPMWFE CZ UIF BDUVBM UZQFT PG BSHVNFOUT SFGFSSFE UP BT SVOUJNF UZQFT  .VMUJNFUIPETEFTDSJCF UIBU UIF EJTQBUDIJOH TUSBUFHZ JT CBTFE PO NVMUJQMF BSHVNFOUT *U IBT BMSFBEZ CFFOBEPQUFE CZ NBOZ MBOHVBHFT JODMVEJOH $PNNPO -JTQ 0CKFDU 4ZTUFN $-04 <%F.JDIJFM
BOE (BCSJFM > %ZMBO <4IBMJU > +VMJB <#F[BOTPO FU BM > FUD;BQQB /BSEFMMJ FU BM <> GPSNBMJTFE +VMJBT NVMUJQMF EJTQBUDIJOH CZ BO FYQSFTTJWF TVCUZQJOH SFMBUJPO ѮF NPTU TQFDJêD NFUIPE GVODUJPO XJMM CF QJDLFE CBTFE PO UIF UZQF PG BSHVNFOUT 6OJPO UZQFT BOE QBSBNFUSJD DPOTUSVDUPST IBWF CFFO VTFE JO UIFJS BQQSPBDI IPXFWFSJOUFSTFDUJPO UZQFT BSF OPU DPOTJEFSFE*O NVMUJNFUIPET BSHVNFOUT BSF SFTPMWFE BU PODF BOE UIF iCFTUNBUDIu CSBODI XJMM CFTFMFDUFE BDDPSEJOH UP TQFDJBMJ[FST )PXFWFS JO PVS DBMDVMJ XF SFTPMWF BSHVNFOUT POF CZ POF
BOE BMM CSBODIFT UIBU DBO BQQMZ BSF TFMFDUFE BOE UIFO SFTVMUT XJMM CF DPNCJOFE ѮF SFTPMVUJPOJO EZOBNJD TFNBOUJDT JT CBTFE PO BOOPUBUJPOTϡ $ĨħĜĥĮĬĢĨħ Ěħĝ 'ĮĭĮīĞ 8ĨīĤϡϚ $ĨħĜĥĮĬĢĨħ*O UIJT UIFTJT XF QSPQPTFE BQQMJDBUJWF TVCUZQJOH B OPWFM TVCUZQJOH BMHPSJUIN UP JOGFS UIFSFUVSO UZQFT PG BQQMJDBUJPO BOE QSPKFDUJPO 8F BMTP EFTJHOFE JUT DPSSFTQPOEJOH KVEHNFOU
BQQMJDBUJWF EJTQBUDIJOH JO UIF EZOBNJD TFNBOUJDT 5PHFUIFS UIFTF GFBUVSFT FOBCMF FYQSFTTJWFDBMDVMJ XJUI B NFSHF PQFSBUPS 8F QSFTFOU B UZQF TPVOE DBMDVMVT UIBU TVQQPSUT BMM GFBUVSFTCVU JT OPOEFUFSNJOJTUJD BOE B TFDPOE EFUFSNJOJTUJD DBMDVMVT XJUI B EJTKPJOUOFTT SFTUSJDUJPOTVQQPSUJOH BMM GFBUVSFT FYDFQU GPS TPNF GPSNT PG PWFSMPBEJOH

ϡϛ 'ĮĭĮīĞ 8ĨīĤ
8F HJWF TPNF EJSFDUJPOT GPS GVUVSF XPSL CFMPXϡϛϚ "ĩĩĥĢĜĚĭĢĨħ .ĨĝĞ
ѮPVHI BQQMJDBUJWF TVCUZQJOH JT B SBUIFS FMFHBOU TPMVUJPO UP FOBCMF UIF PWFSMPBEFE BQQMJDBUJPOSFDPSE QSPKFDUJPO BOE OFTUFE DPNQPTJUJPO BQQMJDBUJPO NPEF TUJMM IBT JUT BEWBOUBHFT JU êUT
JOUP UIF TFUUJOH PG PSEJOBSZ PWFSMPBEJOH BOE IBT UIF QPUFOUJBM GPS CFUUFS UZQF JOGFSFODF BOE
CFTUNBUDI TUSBUFHZ XIJDI XJMM CF FYQBOEFE JO MBUFS QBSBHSBQIT
8F EJTDVTTFE TPNF EFTJHO DIBMMFOHFT JO 4FDUJPO  ѮF JEFBM TPMVUJPO JT UP BEPQU BO
VODPNNPO FWBMVBUJPO PSEFS BOE UP SFEVDF GVODUJPO BQQMJDBUJPO JOUP UIF DBOPOJDBM GPSN MJLF
f a1 a2 ...an  ѮF TZOUBY PG f BOE ai TIPVME CF EFêOFE JO B EFMJDBUF XBZ1ĨĭĞħĭĢĚĥ ĭĨ īĞĝĮĜĞ ĚħħĨĭĚĭĢĨħĬ *O UIF DBMDVMJ TIPXO PVS MBNCEB TZOUBY JT GVMMZ BOOPUBUFE BOE SBUIFS SJHJE UP XSJUF BCBOEPOJOH UIF NBKPS BEWBOUBHFT PG CJEJSFDUJPOBM UZQJOH
"T EJTDVTTFE JO 4FDUJPO  XF DBO VUJMJTF UIF BQQMJDBUJPO NPEF BOE BMMPX VT UP XSJUF UIFFYQSFTTJPO MJLF (λx. x, , λx. (x + 1)) 1 ѮF GVUVSF XPSL JT PO IPX UP EFTJHO B DPSSFTQPOEJOH
EZOBNJD TFNBOUJDT GPS BQQMJDBUJPO NPEF BOE JNQSPWF UIF UZQJOH SVMF UP BMMPX UIF VOBOOPUBUFE TZOUBY $PODMVTJPO BOE 'VUVSF 8PSLϡϛϛ #ĢĝĢīĞĜĭĢĨħĚĥ 5ĲĩĢħĠ
4JODF PVS BQQSPBDI JOGFST CPUI UIF UZQFT PG GVODUJPO BOE BSHVNFOUT XIJDI JT EJĒFSFOU GSPNUIF USBEJUJPOBM CJEJSFDUJPOBM UZQJOH GPS UIF BQQMJDBUJPO DBTF
Γ ' e1 ⇒ A

Γ ' e2 ⇒ B

A#B=C

Γ ' e1 e2 ⇒ C
Γ ' e1 ⇒ A → B

Γ ' e2 ⇐ A

Γ ' e1 e2 ⇒ B

5"ĩĩ

5"ĩĩ

ѮJT BQQSPBDI TBDSJêDFT UIF QPTTJCJMJUZ PG XSJUJOH B TNBSUFS IJHIPSEFS GVODUJPO BQQMJDBUJPO'PS FYBNQMF KT (λx. i`m2) [1, 2] OPUJDF UIBU UIF MBNCEB GVODUJPO JT OPU BOOPUBUFE 
KT : (AMi → "QQH) → [AMi] → ["QQH]*O PVS DBMDVMJ XF OFFE UP XSJUF KT (λx. i`m2 : AMi → "QQH) [1, 2] XIFSF UIF BOOPUBUJPO JT

OPU OFDFTTBSZ GSPN JOUVJUJPO " MJOF PG GVUVSF XPSL JT PO IPX UP SFUBJO UIF BEWBOUBHF PG DIFDLNPEF BOE BMTP QSPWJEF UIF JOGPSNBUJPO PG BSHVNFOUT UP IFMQ JOGFS UIF BQQMJDBUJPO UFSNϡϛϜ "ĦěĢĮĠĮĢĭĢĞĬ
*O $IBQUFS  XF EJTDVTTFE UIF BNCJHVJUJFT BOE QSPWJEFE B SBUIFS OBJWF TPMVUJPO UP QSFWFOU
UIPTF )PXFWFS XIFUIFS PWFSMPEJOH TFNBOUJDT PS EJTKPJOU JOUFSTFDUJPO UZQFT XJMM SFKFDU UIFFYQSFTTJPOT XF DPOTJEFS WBMJE BOE VOBNCJHVPVT'VUVSF XPSL JODMVEFT êOEJOH B EFTJHO UIBU FOBCMFT PWFSMPBEJOH XIJMF QSFTFSWJOH EFUFSNJOJTN ѮFSF BSF TFWFSBM QMBDFT UP EP UIJT 0OF JT UIBU XF DBO FYUFOE UIF EJTKPJOUOFTT TQFD
JêDBUJPO BOE BEBQU JU JO DBTF PG PWFSMPBEJOH "OPUIFS JT XF BEE UIF FYUSB DPOEJUJPO DIFDL JO
BQQMJDBUJWF TVCUZQJOH 'PS UIF MBUUFS XF HBWF TFWFSBM EFTJHO DIPJDFT UIPVHI OPOF PG UIFN
TFSWFT BT B QFSGFDU EFTJHO XIFSF BNCJHVPVT DBTFT BSF GPSCJEEFO XIJMF BMM BQQMJDBCMF DBTFT DBO
CF SFUBJOFEϡϛϝ #ĞĬĭ.ĚĭĜġ "ĩĩīĨĚĜġ
.VMUJNFUIPET BSF SFMBUFE UP PVS XPSL BOE CBTFE PO UIF QSFDJTF SVOUJNF UZQFT 6TVBMMZ NVMUJNFUIPET BEPQU B CFTUNBUDI BQQSPBDI BOE TP JT UIF XPSL PG $BTUBHOB FU BM <> *O PVSDBMDVMJ TIPXO BMM UIF QPTTJCMF CSBODIFT XJMM CF TFMFDUFE )PXFWFS XJUI BQQMJDBUJPO NPEF

 'VUVSF 8PSL
BѫFS BMM BSHVNFOUT BSF DPMMFDUFE XF IBWF UIF QPUFOUJBM UP NPEFM UIF iCFTUNBUDIu BQQSPBDI
BOE BMTP SFVTF UIF TBNF BQQSPBDI JO UIF EZOBNJD TFNBOUJDTϡϛϞ %ĢĬģĨĢħĭ 1ĨĥĲĦĨīĩġĢĬĦ
ѮF DPNCJOBUJPO PG EJTKPJOU JOUFSTFDUJPO UZQFT NFSHF PQFSBUPS BOE QBSBNFUSJD QPMZNPSQIJTN FNQPXFST UIF EJTKPJOU QPMZNPSQIJTN <"MQVJN FU BM > XIJDI MFUT QSPHSBNNFSTTQFDJGZ UIF DPOTUSBJOUT PG UIF UZQF WBSJBCMFT %JTKPJOU QPMZNPSQIJTN DBO FODPEF NBOZ WBMVBCMF GFBUVSFT EZOBNJD NJYJOT QPMZNPSQIJD SFDPSET SPX BOE CPVOEFE QPMZNPSQIJTN <9JF
FU BM > *O UIF GVUVSF XF BSF JOUFSFTUFE JO JOWFTUJHBUJOH IPX UP BQQMZ EJTKPJOU QPMZNPSQIJTN JO PVS DBMDVMJϡϛϟ $ĨĦĩĢĥĞ ĭĨ 3ĚĜĤĞĭ
8F HJWF BO JOUFSQSFUFS JNQMFNFOUBUJPO JO $IBQUFS  XIJDI IFBWJMZ SFMJFT PO UIF 3BDLFUT
SVOUJNF DPOUSBDU DIFDLJOH ѮJT BQQSPBDI EJĒFST GSPN QSBDUJDBM MBOHVBHFT JO UXP BTQFDUT
r 5ZQF DIFDLJOH TIPVME CF TUBUJDBMMZ EPOF BU DPNQJMF UJNF
r 0WFSMPBEJOH BQQMJDBUJPO BOE SFDPSE QSPKFDUJPO TIPVME CF TUBUJDBMMZ SFTPMWFE*O UIF DVSSFOU JNQMFNFOUBUJPO XF POMZ VUJMJTF NJOJNBM QBSUT PG UIF GVODUJPOBMJUJFT PG 3BDLFUTNBDSP TZTUFN BOE EFMFHBUF UIF QBSTJOH BOE FWBMVBUJPO UP UIF GVODUJPOT 8F DBO SFGFS UPTPQIJTUJDBUFE UFDIOJRVFT <$IBOH FU BM  ,JOH > UP FNQMPZ UIF NBDSP TZTUFN UP EFBMXJUI UZQF DIFDLJOH BOE PWFSMPBEJOH SFTPMVUJPO )PXFWFS UIFZ BMM EP OPU BDDPVOU GPS UIFFMBCPSBUJPO TFNBOUJDT PG UIF MBOHVBHF ѮF GVUVSF XPSL JT PO JOWFTUJHBUJOH 3BDLFUT NBDSPTZTUFN UP EFBM XJUI FMBCPSBUJPO BOE CVJMEJOH UIF DPNQJMFS JNQMNFOUBUJPO PG PVS MBOHVBHFT



#ĢěĥĢĨĠīĚĩġĲ<$JUJOH QBHFT BSF MJTUFE BѫFS FBDI SFGFSFODF>+PÈP "MQVJN #SVOP $ E 4 0MJWFJSB BOE ;IJZVBO 4IJ  %JTKPJOU QPMZNPSQIJTN *O&VSPQFBO 4ZNQPTJVN PO 1SPHSBNNJOH 4QSJOHFS m <DJUFE PO QBHF >)FOL #BSFOESFHU .BSJP $PQQP BOE .BSJBOHJPMB %F[BOJ$JBODBHMJOJ  " êMUFS MBNCEBNPEFM BOE UIF DPNQMFUFOFTT PG UZQF BTTJHONFOU ćF KPVSOBM PG TZNCPMJD MPHJD   m <DJUFE PO QBHFT   BOE >+FĒ #F[BOTPO "MBO &EFMNBO 4UFGBO ,BSQJOTLJ BOE 7JSBM # 4IBI  +VMJB " GSFTI BQQSPBDI UP OVNFSJDBM DPNQVUJOH 4*". SFWJFX    m <DJUFE PO QBHF >
9VBO #J #SVOP $ E 4 0MJWFJSB BOE 5PN 4DISJKWFST  ѮF FTTFODF PG OFTUFE DPNQPTJUJPO *O OE &VSPQFBO $POGFSFODF PO 0CKFDU0SJFOUFE 1SPHSBNNJOH &$001  
4DIMPTT %BHTUVIM-FJCOJ[;FOUSVN GVFS *OGPSNBUJL <DJUFE PO QBHFT   BOE >%BOJFM ( #PCSPX -JOEB ( %F.JDIJFM 3JDIBSE 1 (BCSJFM 4POZB & ,FFOF (SFHPS ,JD[BMFT
BOE %BWJE " .PPO  $PNNPO MJTQ PCKFDU TZTUFN TQFDJêDBUJPO "$. 4JHQMBO /PUJDFT
 4*  m <DJUFE PO QBHF >-VDB $BSEFMMJ BOE +PIO $ .JUDIFMM  0QFSBUJPOT PO SFDPSET .BUIFNBUJDBM TUSVDUVSFT JODPNQVUFS TDJFODF    m <DJUFE PO QBHFT  BOE >(JVTFQQF $BTUBHOB (JPSHJP (IFMMJ BOE (JVTFQQF -POHP  " DBMDVMVT GPS PWFSMPBEFEGVODUJPOT XJUI TVCUZQJOH *OGPSNBUJPO BOE $PNQVUBUJPO    m <DJUFEPO QBHFT       BOE >(JVTFQQF $BTUBHOB .JDLBÌM -BVSFOU ,JN /HVZFO BOE .BUUIFX -VU[F  0O UZQF
DBTFT VOJPO FMJNJOBUJPO BOE PDDVSSFODF UZQJOH 1SPDFFEJOHT PG UIF "$. PO 1SPHSBNNJOH-BOHVBHFT  101-   <DJUFE PO QBHF >
4UFQIFO $IBOH "MFY ,OBVUI BOE #FO (SFFONBO  5ZQF TZTUFNT BT NBDSPT *O 1SPDFFEJOHT PG UIF UI "$. 4*(1-"/ 4ZNQPTJVN PO 1SJODJQMFT PG 1SPHSBNNJOH -BOHVBHFTm <DJUFE PO QBHF >#JCMJPHSBQIZ"SUIVS $IBSHVÊSBVE  ѮF MPDBMMZ OBNFMFTT SFQSFTFOUBUJPO +PVSOBM PG BVUPNBUFE SFBTPOJOH    m <DJUFE PO QBHF >"MPO[P $IVSDI  " TFU PG QPTUVMBUFT GPS UIF GPVOEBUJPO PG MPHJD "OOBMT PG NBUIFNBUJDT m <DJUFE PO QBHF >"MPO[P $IVSDI  " GPSNVMBUJPO PG UIF TJNQMF UIFPSZ PG UZQFT ćF KPVSOBM PG TZNCPMJD
MPHJD    m <DJUFE PO QBHF >.BSJP $PQQP .BSJBOHJPMB %F[BOJ$JBODBHMJOJ BOE #FUUJ 7FOOFSJ  'VODUJPOBM DIBSBDUFST PG TPMWBCMF UFSNT .BUIFNBUJDBM -PHJD 2VBSUFSMZ    m <DJUFE PO
QBHFT   BOE >
3PXBO %BWJFT BOE 'SBOL 1GFOOJOH  *OUFSTFDUJPO UZQFT BOE DPNQVUBUJPOBM FĒFDUT *O
1SPDFFEJOHT PG UIF ĕęI "$. 4*(1-"/ JOUFSOBUJPOBM DPOGFSFODF PO 'VODUJPOBM QSPHSBNNJOH m <DJUFE PO QBHF >-JOEB ( %F.JDIJFM BOE 3JDIBSE 1 (BCSJFM  ѮF DPNNPO MJTQ PCKFDU TZTUFN "OPWFSWJFX *O &VSPQFBO $POGFSFODF PO 0CKFDU0SJFOUFE 1SPHSBNNJOH 4QSJOHFS m<DJUFE PO QBHF >%PNJOJRVF %FWSJFTF BOE 'SBOL 1JFTTFOT  0O UIF CSJHIU TJEF PG UZQF DMBTTFT JOTUBODF
BSHVNFOUT JO "HEB "$. 4*(1-"/ /PUJDFT    m <DJUFE PO QBHF >+BOB %VOêFME  &MBCPSBUJOH JOUFSTFDUJPO BOE VOJPO UZQFT +PVSOBM PG 'VODUJPOBM 1SPHSBNNJOH    m <DJUFE PO QBHFT        BOE >+BOB %VOêFME BOE /FFM ,SJTIOBTXBNJ  #JEJSFDUJPOBM UZQJOH "$. $PNQVUJOH 4VSWFZT$463    m <DJUFE PO QBHF >&SJL &SOTU  'BNJMZ QPMZNPSQIJTN *O &VSPQFBO $POGFSFODF PO 0CKFDU0SJFOUFE 1SPHSBNNJOH 4QSJOHFS m <DJUFE PO QBHFT  BOE >
5JN 'SFFNBO BOE 'SBOL 1GFOOJOH  3FêOFNFOU UZQFT GPS .- *O 1SPDFFEJOHT PG UIF "$.
4*(1-"/  DPOGFSFODF PO 1SPHSBNNJOH MBOHVBHF EFTJHO BOE JNQMFNFOUBUJPO m<DJUFE PO QBHF >"MBJO 'SJTDI (JVTFQQF $BTUBHOB BOE 7ÊSPOJRVF #FO[BLFO  4FNBOUJD TVCUZQJOH%FBMJOH TFUUIFPSFUJDBMMZ XJUI GVODUJPO VOJPO JOUFSTFDUJPO BOE OFHBUJPO UZQFT +PVSOBMPG UIF "$. +"$.    m <DJUFE PO QBHF >#JCMJPHSBQIZ+PTFQI " (PHVFO +BNFT 8 ѮBUDIFS &SJD ( 8BHOFS BOE +FTTF # 8SJHIU  *OJUJBM BMHFCSBTFNBOUJDT BOE DPOUJOVPVT BMHFCSBT +PVSOBM PG UIF "$. +"$.    m <DJUFEPO QBHF >
9VFKJOH )VBOH BOE #SVOP $ E 4 0MJWFJSB  " UZQFEJSFDUFE PQFSBUJPOBM TFNBOUJDT GPS
B DBMDVMVT XJUI B NFSHF PQFSBUPS *O UI &VSPQFBO $POGFSFODF PO 0CKFDU0SJFOUFE 1SPHSBNNJOH &$001   4DIMPTT %BHTUVIM-FJCOJ[;FOUSVN GÛS *OGPSNBUJL <DJUFE PO
QBHF >9VFKJOH )VBOH +JOYV ;IBP BOE #SVOP $ E 4 0MJWFJSB  5BNJOH UIF .FSHF 0QFSBUPS+ 'VODU 1SPHSBN   F <DJUFE PO QBHFT          BOE >"UTVTIJ *HBSBTIJ #FOKBNJO $ 1JFSDF BOE 1IJMJQ 8BEMFS  'FBUIFSXFJHIU +BWB B NJOJNBMDPSF DBMDVMVT GPS +BWB BOE (+ "$. 5SBOTBDUJPOT PO 1SPHSBNNJOH -BOHVBHFT BOE 4ZTUFNT
501-"4    m <DJUFE PO QBHF >
4UFGBO ,BFT  1BSBNFUSJD PWFSMPBEJOH JO QPMZNPSQIJD QSPHSBNNJOH MBOHVBHFT *O &V
SPQFBO 4ZNQPTJVN PO 1SPHSBNNJOH 4QSJOHFS m <DJUFE PO QBHFT  BOE >"MFYJT ,JOH 

)BDLFUUMJC

?iiTb,ffTF;bX`+F2i@HM;XQ`;fT+F;2f?+F2ii@HB# <DJUFE PO QBHF >
4UFQIFO $ ,MFFOF BOE + #BSLMFZ 3PTTFS  ѮF JODPOTJTUFODZ PG DFSUBJO GPSNBM MPHJDT"OOBMT PG .BUIFNBUJDT  m <DJUFE PO QBHF >,PBS .BSOUJSPTJBO 5PN 4DISJKWFST #SVOP $ E 4 0MJWFJSB BOE (FPSHJPT ,BSBDIBMJBT 
3FTPMVUJPO BT *OUFSTFDUJPO 4VCUZQJOH WJB .PEVT 1POFOT 1SPD "$. 1SPHSBN -BOH 
0014-" "SUJDMF  OPW   QBHFT <DJUFE PO QBHF >+PIO .D$BSUIZ  3FDVSTJWF GVODUJPOT PG TZNCPMJD FYQSFTTJPOT BOE UIFJS DPNQVUBUJPOCZ NBDIJOF QBSU * $PNNVO "$.    m <DJUFE PO QBHF >
3PCJO .JMOFS  " UIFPSZ PG UZQF QPMZNPSQIJTN JO QSPHSBNNJOH +PVSOBM PG DPNQVUFSBOE TZTUFN TDJFODFT    m <DJUFE PO QBHF >#SVOP $ E 4 0MJWFJSB "ESJBBO .PPST BOE .BSUJO 0EFSTLZ  5ZQF DMBTTFT BT PCKFDUTBOE JNQMJDJUT "$. 4JHQMBO /PUJDFT    m <DJUFE PO QBHF >#SVOP $ E 4 0MJWFJSB ;IJZVBO 4IJ BOE +PBP "MQVJN  %JTKPJOU JOUFSTFDUJPO UZQFT *O
1SPDFFEJOHT PG UIF TU "$. 4*(1-"/ *OUFSOBUJPOBM $POGFSFODF PO 'VODUJPOBM 1SPHSBNNJOH m <DJUFE PO QBHFT  BOE >#JCMJPHSBQIZ#FOKBNJO $ 1JFSDF  1SPHSBNNJOH XJUI JOUFSTFDUJPO UZQFT BOE CPVOEFE QPMZNPSQIJTN
1I% %JTTFSUBUJPO $BSOFHJF .FMMPO 6OJWFSTJUZ <DJUFE PO QBHF >#FOKBNJO $ 1JFSDF BOE %BWJE / 5VSOFS  -PDBM UZQF JOGFSFODF "$. 5SBOTBDUJPOT PO
1SPHSBNNJOH -BOHVBHFT BOE 4ZTUFNT 501-"4    m <DJUFE PO QBHF >(PSEPO % 1MPULJO  " TUSVDUVSBM BQQSPBDI UP PQFSBUJPOBM TFNBOUJDT "BSIVT VOJWFSTJUZ<DJUFE PO QBHF >(BSSFM 1PUUJOHFS  " UZQF BTTJHONFOU GPS UIF TUSPOHMZ OPSNBMJ[BCMF λUFSNT 5P )#$VSSZ FTTBZT PO DPNCJOBUPSZ MPHJD MBNCEB DBMDVMVT BOE GPSNBMJTN  m <DJUFEPO QBHFT  BOE >+PIO $ 3FZOPMET  1SFMJNJOBSZ EFTJHO PG UIF QSPHSBNNJOH MBOHVBHF 'PSTZUIF  <DJUFE PO QBHFT    BOE >+PIO $ 3FZOPMET  ѮF DPIFSFODF PG MBOHVBHFT XJUI JOUFSTFDUJPO UZQFT *O *OUFSOBUJPOBM
4ZNQPTJVN PO ćFPSFUJDBM "TQFDUT PG $PNQVUFS 4PęXBSF 4QSJOHFS m<DJUFE PO

QBHF >+PIO $ 3FZOPMET  %FTJHO PG UIF 1SPHSBNNJOH -BOHVBHF ' PSTZUIF *O "-(0-MJLF
MBOHVBHFT 4QSJOHFS m <DJUFE PO QBHF >/JDIPMBT 3JPVY 9VFKJOH )VBOH #SVOP $ E 4 0MJWFJSB BOE 4UFWF ;EBODFXJD  " #PXUJFGPS B #FBTU 5FDIOJDBM 3FQPSU .4$*4 %FQBSUNFOU PG $PNQVUFS BOE *OGPSNBUJPO
4DJFODF 6OJWFSTJUZ PG 1FOOTZMWBOJB <DJUFE PO QBHF >%BWJE " 4DINJEU  %FOPUBUJPOBM TFNBOUJDT B NFUIPEPMPHZ GPS MBOHVBHF EFWFMPQNFOU
8JMMJBN $ #SPXO 1VCMJTIFST <DJUFE PO QBHF >"OESFX 4IBMJU  ćF %ZMBO SFGFSFODF NBOVBM UIF EFĕOJUJWF HVJEF UP UIF OFX PCKFDUPSJFOUFE EZOBNJD MBOHVBHF "EEJTPO 8FTMFZ -POHNBO 1VCMJTIJOH $P *OD<DJUFE PO

QBHF >1IJMJQ 8BEMFS  ѮF FYQSFTTJPO QSPCMFN 1PTUFE PO UIF +BWB (FOFSJDJUZ NBJMJOH MJTU
  <DJUFE PO QBHFT  BOE >
1IJMJQ 8BEMFS BOE 4UFQIFO #MPUU  )PX UP NBLF BEIPD QPMZNPSQIJTN MFTT BE IPD *O
1SPDFFEJOHT PG UIF UI "$. 4*(1-"/4*("$5 TZNQPTJVN PO 1SJODJQMFT PG QSPHSBNNJOH
MBOHVBHFT m <DJUFE PO QBHFT   BOE >#JCMJPHSBQIZ%BWJE )% 8BSSFO  "QQMJFE MPHJD JUT VTF BOE JNQMFNFOUBUJPO BT B QSPHSBNNJOH UPPM
  <DJUFE PO QBHF >"OESFX , 8SJHIU BOE .BUUIJBT 'FMMFJTFO  " TZOUBDUJD BQQSPBDI UP UZQF TPVOEOFTT*OGPSNBUJPO BOE DPNQVUBUJPO    m <DJUFE PO QBHF >/JOHOJOH 9JF BOE #SVOP $ E 4 0MJWFJSB  -FU "SHVNFOUT (P 'JSTU *O &VSPQFBO 4ZNQPTJVN PO 1SPHSBNNJOH 4QSJOHFS m <DJUFE PO QBHFT  BOE >/JOHOJOH 9JF #SVOP $ E 4 0MJWFJSB 9VBO #J BOE 5PN 4DISJKWFST 

3PX BOECPVOEFE QPMZNPSQIJTN WJB EJTKPJOU QPMZNPSQIJTN *O UI &VSPQFBO $POGFSFODF PO
0CKFDU0SJFOUFE 1SPHSBNNJOH &$001   4DIMPTT %BHTUVIM-FJCOJ[;FOUSVN GÛS *OGPSNBUJL <DJUFE PO QBHF >
8FOKJB :F #SVOP $ E 4 0MJWFJSB BOE 9VFKJOH )VBOH  5ZQF%JSFDUFE 0QFSBUJPOBM
4FNBOUJDT GPS (SBEVBM 5ZQJOH *O UI &VSPQFBO $POGFSFODF PO 0CKFDU0SJFOUFE 1SPHSBNNJOH &$001   4DIMPTT %BHTUVIM-FJCOJ[;FOUSVN GÛS *OGPSNBUJL <DJUFE PO
QBHF >'SBODFTDP ;BQQB /BSEFMMJ +VMJB #FMZBLPWB "SUFN 1FMFOJUTZO #FOKBNJO $IVOH +FĒ #F[BOTPO BOE +BO 7JUFL  +VMJB TVCUZQJOH B SBUJPOBM SFDPOTUSVDUJPO 1SPDFFEJOHT PG UIF"$. PO 1SPHSBNNJOH -BOHVBHFT  0014-"  m <DJUFE PO QBHF >
8FJYJO ;IBOH :BP[IV 4VO BOE #SVOP $ E 4 0MJWFJSB  $PNQPTJUJPOBM 1SPHSBNNJOH
"$. 5SBOTBDUJPOT PO 1SPHSBNNJOH -BOHVBHFT BOE 4ZTUFNT 501-"4    m<DJUFE PO QBHFT  BOE >