" #PXUJF GPS B #FBTU
0WFSMPBEJOH &UB &YQBOTJPO BOE &YUFOTJCMF %BUB 5ZQFT JO F⊲⊳/*$, 3*069 6OJWFSTJUZ PG 1FOOTZMWBOJB 64"
96&+*/( )6"/( BOE #36/0 $ % 4 0-*7&*3" य़F 6OJWFSTJUZ PG )POH ,POH $IJOB
45&7& ;%"/$&8*$ 6OJWFSTJUZ PG 1FOOTZMWBOJB 64"
य़F UZQFE NFSHF PQFSBUPS P੖FST UIF QSPNJTF PG B DPNQPTJUJPOBM TUZMF PG TUBUJDBMMZUZQFE QSPHSBNNJOH JOXIJDI TPMVUJPOT UP UIF FYQSFTTJPO QSPCMFN BSJTF OBUVSBMMZ य़JT BQQSPBDI EVCCFE DPNQPTJUJPOBM QSPHSBNNJOH
IBT SFDFOUMZ CFFO EFNPOTUSBUFE CZ ;IBOH 4VO BOE 0MJWFJSB <>
6OGPSUVOBUFMZ UIF NFSHF PQFSBUPS JT BO VOXJFMEZ CFBTU .FSHJOH WBMVFT GSPN PWFSMBQQJOH UZQFT NBZ CF
BNCJHVPVT TP EJTKPJOUOFTT SFMBUJPOT IBWF CFFO JOUSPEVDFE UP SVMF PVU VOEFTJSFE OPOEFUFSNJOJTN BOE PCUBJOB XFMMCFIBWFE TFNBOUJDT 1BTU UZQF TZTUFNT VTJOH B EJTKPJOU NFSHF PQFSBUPS SFMZ PO JOUFSTFDUJPO UZQFT CVU
FYUFOEJOH TVDI TZTUFNT UP JODMVEF VOJPO UZQFT PS PWFSMPBEFE GVODUJPOT JT QSPCMFNBUJD OBJWFMZ BEEJOH FJUIFSSFJOUSPEVDFT BNCJHVJUZ *O B OVUTIFMM UIF FMJNJOBUJPO GPSNT PG VOJPOT BOE PWFSMPBEFE GVODUJPOT SFRVJSF WBMVFT UP CF EJTUJOHVJTIBCMF CZ DBTF BOBMZTJT CVU UIF NFSHF PQFSBUPS DBO DSFBUF FYPUJD WBMVFT UIBU WJPMBUF UIBUSFRVJSFNFOUय़JT QBQFS QSFTFOUT F⊲⊳ B DPSF MBOHVBHF UIBU EFNPOTUSBUFT IPX VOJPOT JOUFSTFDUJPOT BOE PWFSMPBEJOH DBO
BMM DPFYJTU XJUI B UBNF NFSHF PQFSBUPS य़F LFZ JT BO VOEFSMZJOH EFTJHO QSJODJQMF UIBU TUBUFT UIBU BOZ UXPJOIBCJUFE UZQFT DBO TVQQPSU FJUIFS UIF EFUFSNJOJTUJD NFSHJOH PG UIFJS WBMVFT PS UIF BCJMJUZ UP EJTUJOHVJTI UIFJSWBMVFT CVU OFWFS CPUI 5P SFBMJ[F UIJT JOWBSJBOU XF EFDPNQPTF QSFWJPVTMZ TUVEJFE OPUJPOT PG EJTKPJOUOFTT JOUPUXP OFX EVBM SFMBUJPOT UIBU QFSNJU UIF PQFSBUJPO UIBU CFTU TVJUT FBDI QBJS PG UZQFT य़JT EVBMJUZ SFTQFDUT UIFQPMBSJ[BUJPO PG UIF UZQF TUSVDUVSF ZJFMEJOH BO FYQSFTTJWF MBOHVBHF UIBU XF QSPWF UP CF CPUI UZQF TBGF BOE
EFUFSNJOJTUJD
$$4 $PODFQUT ‫ ۦ‬4PࢄXBSF BOE JUT FOHJOFFSJOH → 'VODUJPOBM MBOHVBHFT %BUB UZQFT BOE TUSVDUVSFT1BUUFSOT ‫ࢊ ۦ‬FPSZ PG DPNQVUBUJPO → 5ZQF UIFPSZ"EEJUJPOBM ,FZ 8PSET BOE 1ISBTFT FYUFOTJCJMJUZ QPMZNPSQIJTN UZQF TZTUFNT"$. 3FGFSFODF 'PSNBU/JDL 3JPVY 9VFKJOH )VBOH #SVOP $ E 4 0MJWFJSB BOE 4UFWF ;EBODFXJD  " #PXUJF GPS B #FBTU 0WFS
MPBEJOH &UB &YQBOTJPO BOE &YUFOTJCMF %BUB 5ZQFT JO F⊲⊳  1SPD "$. 1SPHSBN -BOH  101- "SUJDMF +BOVBSZ   QBHFT IUUQTEPJPSH

 */530%6$5*0/(JWFO UXP QSPHSBNT e1 BOE e2 UIF NFSHF PQFSBUPS e1 ! e2 DPNCJOFT UIFN JOUP POF QSPHSBN UIBU
TVQQPSUT BMM UIF PQFSBUJPOT PG CPUI PG JUT JOQVUT य़JT QPXFSGVM MBOHVBHF GFBUVSF IBT CFFO VTFEUP NPEFM B XJEF SBOHF PG NFDIBOJTNT य़F DBOPOJDBM FYBNQMF JT GPS SFDPSE DPODBUFOBUJPO XIJDI य़JT PQFSBUPS JT TPNFUJNFT XSJ॒FO e , , e JO UIF MJUFSBUVSF CVU XF QSFGFS UIF NPSF TZNNFUSJD ۠!ۡ TJODF UIF PQFSBUPS JT
1
2

DPNNVUBUJWF BOE BTTPDJBUJWF"VUIPST‫ ۝‬BEESFTTFT /JDL 3JPVY OSJPVY!DJTVQFOOFEV 6OJWFSTJUZ PG 1FOOTZMWBOJB 1IJMBEFMQIJB 1FOOTZMWBOJB 64" 9VFKJOH )VBOH YKIVBOH!DTILVIL #SVOP $ E 4 0MJWFJSB CSVOP!DTILVIL य़F 6OJWFSTJUZ PG )POH ,POH )POH ,POH
$IJOB 4UFWF ;EBODFXJD TUFWF[!DJTVQFOOFEV 6OJWFSTJUZ PG 1FOOTZMWBOJB 1IJMBEFMQIJB 1FOOTZMWBOJB 64"1FSNJTTJPO UP NBLF EJHJUBM PS IBSE DPQJFT PG QBSU PS BMM PG UIJT XPSL GPS QFSTPOBM PS DMBTTSPPN VTF JT HSBOUFE XJUIPVU GFFQSPWJEFE UIBU DPQJFT BSF OPU NBEF PS EJTUSJCVUFE GPS QSP੗U PS DPNNFSDJBM BEWBOUBHF BOE UIBU DPQJFT CFBS UIJT OPUJDF BOEUIF GVMM DJUBUJPO PO UIF ੗STU QBHF $PQZSJHIUT GPS UIJSEQBSUZ DPNQPOFOUT PG UIJT XPSL NVTU CF IPOPSFE 'PS BMM PUIFS VTFTDPOUBDU UIF PXOFSBVUIPS T 
i  $PQZSJHIU IFME CZ UIF PXOFSBVUIPS T "35IUUQTEPJPSH
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 





/JDL 3JPVY 9VFKJOH )VBOH #SVOP $ E 4 0MJWFJSB BOE 4UFWF ;EBODFXJDIBT MPOH CFFO VTFE UP NPEFM NVMUJQMF JOIFSJUBODF <$PPL FU BM  8BOE > 'PS JOTUBODF B
NVMUJ੗FME SFDPSE NJHIU CF SFQSFTFOUFE BT UIF NFSHF PG UISFF TJOHMFUPO SFDPSET
e = {l1 ↦→ 1} ! {l2 ↦→ true} ! {l3 ↦→ 3}*O B UZQFE TF॒JOH POF BTTJHOT NFSHFT JOUFSTFDUJPO UZQFT य़VT e IBT UIF UZQF {l1 : Int} # {l2 :Bool} # {l3 : Int} )FSF XF BSF BTTVNJOH UIF SFDPSE ੗FMET BSF BMM EJTUJODU l1 ≠ l2 ≠ l3 
6OGPSUVOBUFMZ UIF NFSHF PQFSBUPS IBT B DPTU NFSHFT PG BSCJUSBSZ WBMVFT MFBE UP OPOEFUFSNJOJTN'PS FYBNQMF XIJMF NFSHJOH SFDPSET XJUI EJTUJODU ੗FMET BT JO UIF QSPHSBN e BCPWF JT QFSGFDUMZ SFBTPOBCMF NFSHJOH UIF CPPMFBO WBMVFT true BOE false XPVME SFRVJSF UIF FYJTUFODF PG B UIJSE CPPMFBOWBMVF UIBU JT CPUI true BOE false य़JT WJPMBUFT QSPHSBNNFST‫ ۝‬FYQFDUBUJPO UIBU POMZ POF CSBODI PG BO
JG TUBUFNFOU XJMM FYFDVUF B QSPHSBN MJLF if true ! false then e1 else e2 JT BNCJHVPVT 8F XPVME MJLF
B XBZ UP FOBCMF UIF QPXFS PG UIF NFSHF PQFSBUPS XIJMF EJTBMMPXJOH OPOEFUFSNJOJTUJD QSPHSBNTMJLF UIJT POF0MJWFJSB FU BM <> JOUSPEVDF B UZQJOH EJTDJQMJOF GPS UIF NFSHF PQFSBUPS UIBU SVMFT PVU TVDI
OPOEFUFSNJOJTUJD QSPHSBNT VTJOH EJTKPJOU JOUFSTFDUJPO UZQFT 6OEFS TVDI B UZQJOH EJTDJQMJOF POMZ
FYQSFTTJPOT XJUI EJTKPJOU UZQFT DBO CF NFSHFE 4JODF Bool JT OPU EJTKPJOU GSPN JUTFMG UIF NFSHF
true ! false JT SFKFDUFE य़JT MJOF PG XPSL MFE UP TVDDFTT JO UIF NPEFMJOH PG B OVNCFS PG IJHIMZDPNQPTJUJPOBM QSPHSBNNJOH QB॒FSOT JODMVEJOH GPSNT PG GBNJMZ QPMZNPSQIJTN <&SOTU > BOEटSTUDMBTT USBJUT <#J BOE 0MJWFJSB > *U IBT DVMNJOBUFE JO MBOHVBHFT UIBU TVQQPSU B TUZMF PG QSPHSBNNJOH LOPXO BT DPNQPTJUJPOBM QSPHSBNNJOH <;IBOH FU BM > XIJDI P੖FST TPMVUJPOT UPDIBMMFOHFT TVDI BT UIF &YQSFTTJPO 1SPCMFN <8BEMFS > "U UIF IFBSU PG UIFTF EFTJHOT JT UIF BCJMJUZ PG UIF NFSHF PQFSBUPS UP TVQQPSU OFTUFE DPNQPTJUJPO <#J FU BM > XIJDI FYQMPJUT TVCUZQJOHSFMBUJPOTIJQT MJLF
(Int → {age : Int}) # (Int → {name : String})≤

Int → {age : Int, name : String})FSF UIF NFSHF PQFSBUPS MFUT VT DPNCJOFDPNQPTF UIF CFIBWJPS PG NVMUJQMF JNQMFNFOUBUJPOT *G
XF UIJOL PG UIF UXP GVODUJPOT JO UIF JOUFSTFDUJPO BT DPOTUSVDUPST PG PCKFDUT XIBU POF HFUT PVU JT B
OFX DPOTUSVDUPS GPS PCKFDUT XJUI UIF DPNCJOFE CFIBWJPST"U UIF TBNF UJNF UIF NFSHF PQFSBUPS IBT BMTP CFFO TIPXO UP TVQQPSU B GPSN PG GVODUJPO PWFSMPBEJOH JO XIJDI B TJOHMF GVODUJPO DBO IBWF TFWFSBM CPEJFT BOE UIF DIPJDF PG XIJDI UP SVO JT
EFUFSNJOFE CZ JUT BSHVNFOUT <$BTUBHOB FU BM  %VO੗FME  1JFSDF B> य़F NFSHF PQFSBUPS DBO DPNCJOF NVMUJQMF JNQMFNFOUBUJPOT PG GVODUJPOT UIBU UBLF EJ੖FSFOU BSHVNFOU UZQFT -BUFSUIF BQQSPQSJBUF JNQMFNFOUBUJPO DBO CF EJTQBUDIFE UP CBTFE PO UIF BSHVNFOU BU UIF BQQMJDBUJPOTJUF )PXFWFS PWFSMPBEJOH DBO BMTP FBTJMZ MFBE UP OPOEFUFSNJOJTN JG OPU DBSFGVMMZ NBOBHFE
#PUI PG UIFTF GFBUVSFT OFTUFE DPNQPTJUJPO BOE PWFSMPBEJOH BSF JOEFQFOEFOUMZ VTFGVM CVU TP GBS
OP TZTUFN BDDPNNPEBUFT UIFN TJNVMUBOFPVTMZ य़F UZQJOH EJTDJQMJOF VTFE GPS UIF NFSHF PQFSBUPSJO 0MJWFJSB‫۝‬T MJOF PG XPSL EPFT OPU TVQQPSU USBEJUJPOBM GPSNT PG PWFSMPBEJOH BOE DPOWFSTFMZ UIFTZTUFNT UIBU TVQQPSU PWFSMPBEJOH EP OPU TVQQPSU OFTUFE DPNQPTJUJPO य़JT JT UIF ੗STU QSPCMFN UIBUXF BEESFTT JO UIJT QBQFS
"OPUIFS OBUVSBM GFBUVSF UP DPOTJEFS BMPOHTJEF PWFSMPBEJOH JT VOJPO UZQFT <#BSCBOFSB FU BM >
A % B JT UIF VOUBHHFE VOJPO PG A BOE B #PUI A WBMVFT BOE B WBMVFT IBWF UIJT UZQF CFDBVTF FHA ≤ A % B CVU VOMJLF GPS UBHHFE VOJPOT UIFSF JT OP FYUSB EZOBNJD JOGPSNBUJPO B॒BDIFE UP UIFWBMVF UP SFWFBM XIJDI DBTF JU JT /FWFSUIFMFTT UIF DPOTUSVDUPST PG WBMVFT PG UZQF A XJMM PॏFO CF
EJTUJODU GSPN UIPTF PG UZQF B XIJDI JT TVਖ਼DJFOU UP UFMM UIFN BQBSU 'PS PVS QVSQPTFT XF BTTVNFUIBU UIF DPOTUSVDUPST PG CBTF UZQFT MJLF Int BSF EJTKPJOU GSPN UIPTF PG PUIFS CBTF UZQFT MJLF BoolTP 1 BOE true BSF EJTUJODU *O PUIFS XPSET B QSPHSBNNFS DBO VTF B QB॒FSONBUDIJOH DPOTUSVDU UPFMJNJOBUF B WBMVF e PG UZQF Int % Bool BT GPMMPXT
match e with {(x1 : Int) ↦→ true, (x2 : Bool) ↦→ false}

1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

" #PXUJF GPS B #FBTU

*G e = 1 : Int UIFO JU JT EJTUJODU GSPN UIF DPOTUSVDUPST PG Bool TP UIF NBUDI BCPWF XJMM XPSLBT JOUFOEFE BOE FWBMVBUF UP true -JLFXJTF JG e = true : Bool UIF NBUDI XJMM FWBMVBUF UP false
TP QB॒FSO NBUDIJOH EJTDSJNJOBUFT CFUXFFO Int BOE Bool WBMVFT BT FYQFDUFE 6OGPSUVOBUFMZ JO UIFQSFTFODF PG UIF NFSHF PQFSBUPS UIFSF JT B QSPCMFN UIF UFSN e = 1 ! true IBT UZQF Int # Bool XIJDIJT B TVCUZQF PG Int % Bool /PX UP EFDJEF XIFUIFS e JT BO Int PS B Bool EVSJOH QB॒FSO NBUDIJOHZJFMET UIF BOTXFS UIBU JU JT CPUI MFBEJOH BHBJO UP OPOEFUFSNJOJTUJD FWBMVBUJPO 4BGFMZ JODPSQPSBUJOHVOJPO UZQFT XJUI JOUFSTFDUJPOT BOE UIF NFSHF PQFSBUPS JT UIF TFDPOE QSPCMFN XF BEESFTT%JTKPJOUOFTT BOE QPMBSJUZ य़JT QBQFS HJWFT B TPMVUJPO UP CPUI PG UIF QSPCMFNT NFOUJPOFE BCPWF
य़F LFZ JEFB JT UIBU GPS DFSUBJO UZQFT MJLF Int BOE Bool BCPWF QB॒FSO NBUDIJOH QSPWJEFT B NFDIBOJTN GPS EJTUJOHVJTIJOH UIFJS WBMVFT 8IFO UIFSF JT TVDI B NFDIBOJTN GPS UZQFT A BOE B XF TBZ A
BOE B BSF EJTUJOHVJTIBCMF XSJ॒FO A ⊳⊲ B 0VS MBOHVBHF EFTJHO SFRVJSFT UIBU QB॒FSOT JO EJ੖FSFOU
CSBODIFT PG B NBUDI DPOTUSVDU NBUDI EJTUJOHVJTIBCMF UZQFT 5ZQFT UIBU BSF FMJNJOBUFE WJB QB॒FSONBUDIJOH BSF OBUVSBMMZ EJTUJOHVJTIBCMF GSPN FBDI PUIFS TVDI UZQFT BSF DBMMFE QPTJUJWF JO UIF MJUFSBUVSF PO QPMBSJ[FE UZQF UIFPSZ <"OESFPMJ > *OUVJUJWFMZ UIF WBMVFT PG TVDI UZQFT BSF EF੗OFE
DPNQMFUFMZ CZ IPX UIFZ BSF DPOTUSVDUFE BOE QB॒FSO NBUDIJOH FYUSBDUT BMM PG UIF JOGPSNBUJPOBCPVU UIFN
0O UIF ੘JQ TJEF GVODUJPOT BSF DIBSBDUFSJ[FE WJB B ۠TUSPOHۡ JF OPONBUDIJOH FMJNJOBUJPO GPSNय़FZ BSF DIBSBDUFSJ[FE FYUFOTJPOBMMZ CZ UIF DPOUFYUT JO XIJDI UIFZ BSF VTFE OPU CZ IPX UIFZ BSF
DPOTUSVDUFE य़JT NFBOT UIBU GVODUJPO UZQFT BSF OFHBUJWF /FHBUJWF UZQFT BSF SFMFWBOU CFDBVTF UP
PVS LOPXMFEHF BMM QSBDUJDBM VTFT PG UIF NFSHF PQFSBUPS JO UIF MJUFSBUVSF DPODFSO NFSHFT PG OFHBUJWFUZQFT 5P BQQMZ UIF NFSHF PQFSBUPS UP UXP BSHVNFOUT PG UZQFT A BOE B PVS EFTJHO SFRVJSFT UIBU A
BOE B BSF NFSHFBCMF XSJ॒FO A ⊲⊳ B
5PHFUIFS UIFTF UXP SFMBUJPOT EFTDSJCF XIFO JU JT VOBNCJHVPVT UP NFSHF UXP GVODUJPOT UP DSFBUF
BO PWFSMPBEFE GVODUJPO 'PS FYBNQMF JU NBLFT TFOTF GPS UXP GVODUJPO UZQFT TVDI BT Int → String
BOE Bool → String UP CF NFSHFBCMF CFDBVTF UIFJS JOQVUT BSF EJTUJOHVJTIBCMF .PSFPWFS BT UZQJDBMMZ BMCFJU OPU VOJWFSTBMMZ EFTDSJCFE JO MBNCEB DBMDVMJ B GVODUJPO EPFT OPU QSPWJEF B NFBOT PG
EZOBNJDBMMZ BTLJOH XIFUIFS JU BDDFQUT JOUFHFST PS TUSJOHT BT JOQVUT य़VT GSPN UIJT QFSTQFDUJWFXF XPVME OPU FYQFDU UIF UZQF Int → String UP CF EJTUJOHVJTIBCMF GSPN UIF UZQF Bool → String
BOE JO PVS TZTUFN UIFZ BSF OPU EJTUJOHVJTIBCMF
8F SFGFS UP CPUI EJTUJOHVJTIBCJMJUZ BOE NFSHFBCJMJUZ BT EJTKPJOUOFTT SFMBUJPOT UIF GPSNFS JT UIFEJTKPJOUOFTT PG UZQFT BT TFUT PG WBMVFT BOE UIF MB॒FS JT UIF EJTKPJOUOFTT PG UZQFT BT TFUT PG UIFJSDPOUFYUT JF UIF PQFSBUJPOT UIBU DBO CF DBSSJFE PVU PO UIFJS WBMVFT " LFZ JOWBSJBOU PG PVS MBOHVBHF EFTJHO JT UIBU OP UXP JOIBCJUFE UZQFT BSF CPUI EJTUJOHVJTIBCMF
BOE NFSHFBCMFۘUIFZ DBO CF POMZ POF PS UIF PUIFS य़JT EJTDJQMJOF SVMFT PVU UIF JTTVFT PG OPOEFUFSNJOJTN UIBU BSJTF JO UIF QSFTFODF PG CPUI JOUFSTFDUJPO BOE VOJPO UZQFT 'PS JOTUBODF UIJT QSJODJQMF
SVMFT PVU UIF BNCJHVPVT NBUDI GPS e = 1 ! true TJODF Int BOE Bool BSF EJTUJOHVJTIBCMF CVU UIFZBSF OPU NFSHFBCMF BOE e JT JMM UZQFE *OEFFE UIFSF JT OP UFSN PG UIF UZQF Int # Bool BOE XF EP OPU
FWFO DPOTJEFS UIBU UZQF UP CF XFMM GPSNFE य़F PCTFSWBUJPOT UIBU XF IBWF NBEF BCPVU QPMBSJUZ
TVHHFTU B OBUVSBM BOTXFS UP UIF RVFTUJPO PG XIFUIFS B QBJS PG UZQFT TIPVME CF EJTUJOHVJTIBCMF QPTJUJWF PS NFSHFBCMF OFHBUJWF  0VS UZQF TZTUFN FYQMPJUT UIJT PCTFSWBUJPO UP DSFBUF BO FYQSFTTJWFZFU EFUFSNJOJTUJD QSPHSBNNJOH MBOHVBHF
$POUSJCVUJPOT 0VS QSJNBSZ SFTVMU JT UIF GPSNBMJ[BUJPO PG B DPSF MBOHVBHF F⊲⊳ QSPOPVODFE ۠'
CPXۡ  8F QSPWF UIF UZQF TZTUFN TPVOE BOE EFNPOTUSBUF JUT TVQQPSU GPS DPNQPTJUJPOBM QSPHSBNNJOH F⊲⊳ TIPXDBTFT TFWFSBM JNQPSUBOU BTQFDUT
• *U JT UIF ੗STU MBOHVBHF UP JODMVEF EJTKPJOU JOUFSTFDUJPO BOE VOJPO UZQFT PWFSMPBEJOH BOE B
EFUFSNJOJTUJD NFSHF PQFSBUPS य़FTF GFBUVSFT DPNCJOF UP QFSNJU VTFT PG OFTUFE DPNQPTJUJPO
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

/JDL 3JPVY 9VFKJOH )VBOH #SVOP $ E 4 0MJWFJSB BOE 4UFWF ;EBODFXJD• *U JT BMTP B TUFQ UPXBSET JODPSQPSBUJOH UIF XPSL PG $BTUBHOB (IFMMJ BOE -POHP JOUP UIFMJUFSBUVSF PO EJTKPJOU JOUFSTFDUJPO UZQFT <0MJWFJSB FU BM >
• "T JO QBTU USFBUNFOUT PG UIF NFSHF PQFSBUPS UIF PQFSBUJPOBM TFNBOUJDT JT UZQFEJSFDUFE <)VBOH
FU BM > )PXFWFS UZQF JOGPSNBUJPO JT OPU VTFE GPS TFMFDUJOH XIJDI PWFSMPBE UP FYFDVUF
BU B DBMM TJUF *O F⊲⊳ EJTQBUDI JT DP QB॒FSO NBUDIJOH $POTFRVFOUMZ XF DIBSBDUFSJ[F UIFEZOBNJD SPMF PG UZQFT BT SVOUJNF 𝜂FYQBOTJPO• य़F UZQF TZTUFN EFNPOTUSBUFT UIF EVBM DPODFQUT PG NFSHFBCJMJUZ BOE EJTUJOHVJTIBCJMJUZ #PUIIBWF CFFO TUVEJFE JOEFQFOEFOUMZ <0MJWFJSB FU BM  3FINBO FU BM > CVU IFSF JU JT
TIPXO UIBU JO UBOEFN UIFZ FOBCMF XFMMUZQFE EFUFSNJOJTUJD PWFSMPBEJOHय़F LFZ UFDIOJDBM SFTVMUT JO UIJT QBQFS IBWF CFFO QSPWFO VTJOH B DPNCJOBUJPO PG QFODJMBOE
QBQFS QSPPGT GPS UIF SFTVMUT IBWJOH UP EP XJUI UIF UFSN MBOHVBHF DPOTUSVDUT BOE B $PR EFWFMPQNFOU य़F QBQFS QSPPGT BSF BWBJMBCMF JO UIJT BSUJDMF‫۝‬T DPNQBOJPO UFDIOJDBM BQQFOEJY <3JPVY FU BMC> य़F $PR EFWFMPQNFOU <3JPVY FU BM B> GPSNBMJ[FT DFSUBJO UZQFMFWFM QBSUT PG UIF TFNBOUJDT JODMVEJOH TVCUZQJOH EJTQBUDI BOE TPNF LFZ QSPQFSUJFT PG EJTKPJOUOFTT

07&37*&8

य़JT TFDUJPO HJWFT BO PWFSWJFX PG UIJT QBQFS TUBSUJOH XJUI CBDLHSPVOE PO NFSHFT BOE EJTKPJOUJOUFSTFDUJPO UZQFT BOE UIFO JOUSPEVDJOH UIF LFZ JEFBT PG PVS XPSL#BDLHSPVOE*OUFSTFDUJPO BOE VOJPO UZQFT *OUFSTFDUJPO BOE VOJPO UZQFT <#BSCBOFSB FU BM  $PQQP BOE%F[BOJ$JBODBHMJOJ  1P॒JOHFS > BSF XJEFMZ VTFE JO EJWFSTF ੗FMET PG QSPHSBNNJOH MBOHVBHFT *OUFSTFDUJPO UZQFT XFSF JOUSPEVDFE UP DIBSBDUFSJ[F FYBDUMZ BMM TUSPOHMZ OPSNBMJ[JOH MBNCEBUFSNT 6OJPO UZQFT XFSF MBUFS JOUSPEVDFE BT UIF EVBM DPOTUSVDU PG JOUFSTFDUJPO UZQFT <#BSCBOFSB
FU BM > *OUFSTFDUJPO UZQFT XFSF ੗STU BEPQUFE GPS QSPHSBNNJOH CZ XPSL PO 'PSTZUIF <3FZOPMET > BOE TVCTFRVFOUMZ FNQMPZFE UP FYQSFTT LFZ BTQFDUT PG NVMUJQMF JOIFSJUBODF <$PN
QBHOPOJ BOE 1JFSDF > JO PCKFDUPSJFOUFE QSPHSBNNJOH य़F 4DBMB MBOHVBHF <0EFSTLZ FU BM
> BOE JUT %05 DBMDVMVT <3PNQG BOE "NJO > GPS FYBNQMF NBLF GVOEBNFOUBM VTF PG JOUFSTFDUJPO UZQFT UP FYQSFTT B DMBTTUSBJU UIBU FYUFOET NVMUJQMF PUIFS USBJUT 6OJPO UZQFT IBWF BMTP CFFOBEPQUFE JO QSPHSBNNJOH MBOHVBHFT 'PS JOTUBODF UIFZ BSF XJEFMZ VTFE JO 5ZQF4DSJQU BOE 'MPX
BOE XFSF BMTP JODMVEFE JO 4DBMB ࡋF NFSHF PQFSBUPS य़F 'PSTZUIF MBOHVBHF <3FZOPMET  > JOUSPEVDFE B NFSHF PQFSBUPSXIJDI BMMPXT CVJMEJOH WBMVFT UIBU DBO IBWF NVMUJQMF UZQFT FYQSFTTFE BT JOUFSTFDUJPO UZQFT  य़F
NFSHF PQFSBUPS IBT CFFO TUVEJFE NPSF SFDFOUMZ CZ %VO੗FME <> XIP SFNPWFE TJHOJ੗DBOU SF
TUSJDUJPOT PSJHJOBMMZ QSFTFOU JO 3FZOPMET‫ ۝‬EFTJHO " TJNQMF FYBNQMF PG B QSPHSBN VTJOH UIF NFSHF
PQFSBUPS JT
let f = isDigit ! OPU in (f ‘1‫۝‬, f false))FSF f JT BO PWFSMPBEFE GVODUJPO UIBU DBO UBLF FJUIFS B DIBSBDUFS PS B CPPMFBO BT BO BSHVNFOU JU
IBT UIF UZQF (Char → Bool) # (Bool → Bool) य़F WBSJBCMF f JT CVJMU VTJOH UIF NFSHF PQFSBUPSBOE BQQMZJOH JU FYUSBDUT POF PG UIF GVODUJPOT GSPN UIF NFSHFE WBMVF *O UIF CPEZ PG UIF let XF TFF
UXP BQQMJDBUJPOT PG f  POF UP B DIBSBDUFS BOE BOPUIFS UP B CPPMFBO य़JT TUZMF PG PWFSMPBEJOH JT POF
PG UIF NBKPS GFBUVSFT PG UIF NFSHF PQFSBUPS UIBU IBT CFFO FYQMPSFE JO FBSMJFS SFTFBSDI <$BTUBHOB %VO੗FME > *O BEEJUJPO UP PWFSMPBEJOH XF DBO FYQSFTT NVMUJ੗FME SFDPSET CZ NFSHJOH
TJOHMF੗FME SFDPSET BT BMSFBEZ NFOUJPOFE JO UIF JOUSPEVDUJPO 
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

" #PXUJF GPS B #FBTU$PNQPTJUJPOBM QSPHSBNNJOH BOE OFTUFE DPNQPTJUJPO 3FDFOU SFTFBSDI PO UIF NFSHF PQFSBUPSTIPXT UIBU JU BMTP FOBCMFT टSTUDMBTT DMBTTFTUSBJUT <#J BOE 0MJWFJSB > BOE DPNQPTJUJPOBM QSPHSBNNJOH <;IBOH FU BM > $PNQPTJUJPOBM QSPHSBNNJOH TVQQPSUT FYUFOTJCMF GPSNT PG EBUBUZQFT
BOE GVODUJPOT BOE P੖FST B OBUVSBM TPMVUJPO UP IBSE NPEVMBSJUZ DIBMMFOHFT TVDI BT UIF &YQSFTTJPO
1SPCMFN <8BEMFS > "U UIF IFBSU PG DPNQPTJUJPOBM QSPHSBNNJOH JT B NFDIBOJTN DBMMFE OFTUFEDPNQPTJUJPO <#J FU BM > UIBU DPNQPTFT CFIBWJPS GSPN NVMUJQMF DPNQPOFOUT JO B NFSHF /FTUFEDPNQPTJUJPO EJ੖FST GSPN PWFSMPBEJOH PS TJNQMF SFDPSE QSPKFDUJPO XIJDI TFMFDU POMZ POF PG UIFDPNQPOFOUT JO B NFSHF 8JUI OFTUFE DPNQPTJUJPO XF DBO XSJUF
let mkStudent = (𝜆𝑛 : Int. {age ↦→ 𝑛}) ! (𝜆𝑛 : Int. {idNumber ↦→ . . .}) in mkStudent 25*O UIJT DBTF XF DPNCJOF UXP GVODUJPOT XJUI B NFSHF UP HFU BO FYQSFTTJPO XJUI UIF UZQF
(Int → {age : Int}) # (Int → {idNumber : Int})

6TJOH TVCUZQJOH mkStudent DBO CF HJWFO UIF GVODUJPO UZQF Int → {age : Int, idNumber : Int}
PQFSBUJPOBMMZ UIF TFNBOUJDT PG NFSHF DPNCJOFT UIF UXP GVODUJPOT य़VT XF DBO VTF mkStudent UP
CVJME B OFX SFDPSE UIBU IBT CPUI BO age BOE B idNumber ੗FME
.FSHFT "NCJHVJUZ BOE 4VCUZQJOH य़F JOUFSBDUJPO CFUXFFO TVCUZQJOH BOE UIF NFSHF PQFSBUPSJT TVCUMF 5P JMMVTUSBUF UIF JTTVF XF VTF BO FYBNQMF TJNJMBS UP POF HJWFO CZ $BSEFMMJ BOE .JUDIFMM<>
𝑒 ! = let x : {l2 : Bool} = {l1 ↦→ 1, l2 ↦→ true} in ({l1 ↦→ 2} ! x).l1 + 3*O UIJT QSPHSBN x IBT UZQF {l2 : Bool} EFTQJUF BMTP JODMVEJOH B ੗FME l1  य़F ੗FME l1 JT IJEEFO EVF
UP TVCUZQJOH CFDBVTF {l1 : Int, l2 : Bool} ≤ {l2 : Bool} य़F NFSHF {l1 ↦→ 2} ! x BQQFBST UP CFTBGF TUBUJDBMMZ CFDBVTF UIF UZQF PG x EPFT OPU DPOUBJO l1  )PXFWFS XIBU TIPVME IBQQFO XIFO XF
QSPKFDU l1 *G UIF PSJHJOBM ੗FME l1 JT QSFTFSWFE JO x UIFO XIFO XF MBUFS MPPLVQ l1 UIFSF XJMM CF UXP l1
੗FMET *G XF VTF B CJBTFE MPPLVQ XIJDI SFUVSOT FJUIFS UIF ੗STU WBMVF GSPN UIF MFॏ PS UIF ੗STU WBMVF
GSPN UIF SJHIU JO B NFSHF UIFO UIF TFNBOUJDT PG QSPHSBNT NBZ MFBE UP TVSQSJTJOH CFIBWJPVS 'PS
JOTUBODF JO UIF QSPHSBN BCPWF JG B SJHIUCJBTFE MPPLVQ JT VTFE UIFO UIF QSPHSBN XPVME SFUVSO 4)PXFWFS B QSPHSBNNFS NBZ IBWF FYQFDUFE 5 BT B SFTVMU CFDBVTF UIF UZQF PG x BQQFBST UP QSPNJTFUIBU OP ੗FME l1 JT QSFTFOU .PSFPWFS JG UIF UZQFT PG UIF UXP 𝑙 1 ੗FMET BSF EJTUJODU UIJT QSPHSBN DPVME
MFBE UP B SVOUJNF UZQFFSSPS XIFO UIF ੗FME PG UIF XSPOH UZQF JT QSPKFDUFE VOMFTT TQFDJBM DBSF JOUBLFO UP QSFWFOU TVDI B TJUVBUJPO *O FTTFODF XF XPVME MJLF UIBU JOGPSNBUJPO IJEEFO WJB TVCUZQJOHIBT OP F੖FDU JO MBUFS VTFT PG WBMVFT XJUI IJEEFO JOGPSNBUJPO 'PS UIJT SFBTPO $BSEFMMJ BOE .JUDIFMM
BSHVFE UIBU CJBTFE MPPLVQT TIPVME OPU CF VTFE .PSF EFUBJMFE EJTDVTTJPOT BCPVU TVDI JTTVFT DBO
CF GPVOE JO XPSL CZ )VBOH FU BM <>
%JTKPJOU *OUFSTFDUJPO 5ZQFT 5P BEESFTT UIF BNCJHVJUZ QSPCMFNT BT XFMM BT UIF QSPCMFNT BSJTJOH
GSPN UIF JOUFSBDUJPOT CFUXFFO NFSHFT BOE TVCUZQJOH 0MJWFJSB FU BM <> QSPQPTFE UP SFTUSJDU
NFSHFT TP UIBU POMZ NFSHFBCMF UZQFT BSF BDDFQUFE %JTKPJOUOFTT SFKFDUT BNCJHVPVT QSPHSBNT TVDI
BT true ! false CFDBVTF UIF UZQFT PG UIF UXP WBMVFT CFJOH NFSHFE BSF OPU EJTKPJOU .PSFPWFSEJTKPJOUOFTT FOTVSFT UIBU UIF NFSHF PQFSBUPS JT TZNNFUSJD PS VOCJBTFE HVBSBOUFFJOH CPUI UIFBTTPDJBUJWJUZ BOE DPNNVUBUJWJUZ PG UIF PQFSBUPS
0SJHJOBMMZ UIF TFNBOUJDT PG UIF NFSHF PQFSBUPS XJUI EJTKPJOU JOUFSTFDUJPO UZQFT XBT EF੗OFECZ FMBCPSBUJPO GPMMPXJOH UIF BQQSPBDI QSPNPUFE CZ %VO੗FME <> .PSF SFDFOUMZ )VBOH FU BM
<> QSPQPTFE B UZQFEJSFDUFE PQFSBUJPOBM TFNBOUJDT य़JT BQQSPBDI HJWFT B EJSFDU PQFSBUJPOBMTFNBOUJDT UP 𝜆𝑖 XIJDI JT B DBMDVMVT XJUI EJTKPJOU JOUFSTFDUJPO UZQFT BOE UIF NFSHF PQFSBUPS *O 𝜆𝑖
QSPHSBNT DBO SFEVDF XJUIPVU FODPVOUFSJOH BNCJHVJUJFT JO UIF NFSHFT
8JUI B UZQFEJSFDUFE PQFSBUJPOBM TFNBOUJDT UZQFT BSF SFMFWBOU BU SVOUJNF BOE UIFZ BSF VTFEUP FOGPSDF UIF JOGPSNBUJPO IJEJOH QSPNJTFE CZ TVCUZQJOH $POTJEFS BHBJO 𝑒 ! UIF QSPHSBN EF੗OFE
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

/JDL 3JPVY 9VFKJOH )VBOH #SVOP $ E 4 0MJWFJSB BOE 4UFWF ;EBODFXJDQSFWJPVTMZ *O UIJT DBTF XF ESPQ UIF ੗FME l1 JO x XIFO UIF WBMVF JT DBTU UP UIF UZQF {l2 : Bool}
य़FSFGPSF ({l1 ↦→ 2} ! x).l1 XPVME CFDPNF ({l1 ↦→ 2} ! {l2 ↦→ true}).l1 BOE UIF ੗OBM SFTVMU PG
UIF QSPHSBN XPVME CF 5 *O PUIFS XPSET UIJT TPMVUJPO UP UIF QSPCMFN PG UIF JOUFSBDUJPO CFUXFFO
NFSHFT BOE TVCUZQJOH FOTVSFT UIBU DPNQPOFOUT PG B NFSHF UIBU BSF IJEEFO CZ TVCUZQJOH BSF OP
MPOHFS BDDFTTJCMF GSPN UIF WBMVF BॏFS VQDBTUJOH
8IJMF UIF FYJTUJOH BQQSPBDIFT UP EJTKPJOUOFTT DBO EFBM XJUI QSPHSBNT UIBU IBWF NFSHFT PG
SFDPSET PS UIBU VTF OFTUFE DPNQPTJUJPO UIFZ IBWF SFTUSJDUFE TVQQPSU GPS PWFSMPBEJOH 'PS JOTUBODFUIF NFSHF VTFE JO UIF EF੗OJUJPO PG UIF PWFSMPBEFE GVODUJPO f JF isDigit ! OPU XPVME CF SFKFDUFE*O FTTFODF JO UIF OPUJPO PG EJTKPJOUOFTT QSPQPTFE CZ 0MJWFJSB FU BM <0MJWFJSB FU BM > UXP GVODUJPOT BSF EJTKPJOU JG UIFJS SFUVSO UZQFT BSF EJTKPJOU )PXFWFS Char → Bool BOE Bool → Bool IBWFPWFSMBQQJOH SFUVSO UZQFT य़F EJTKPJOUOFTT SFTUSJDUJPO DPOUSBTUT XJUI USBEJUJPOBM BQQSPBDIFT XJUIPWFSMPBEJOH XIFSF EJTUJODU JOQVU UZQFT BSF VTFE UP FMJNJOBUF QPTTJCMF BNCJHVJUJFT GPS PWFSMPBEFEGVODUJPOT *O BEEJUJPO OPOF PG UIF FYJTUJOH DBMDVMJ XJUI EJTKPJOU JOUFSTFDUJPO UZQFT JODMVEF VOJPOUZQFT XIJDI JOUSPEVDF OFX BNCJHVJUZ JTTVFT$IBMMFOHFT GPS %FUFSNJOJTUJD .FSHFT XJUI 0WFSMPBEJOH BOE 6OJPO 5ZQFT

6OJPO 5ZQFT *O QSJPS BQQSPBDIFT BT FYFNQMJ੗FE CZ 𝜆𝑖 UIF UFSN 1 ! true JT B XFMMUZQFE NFSHF
य़JT JT CFDBVTF UIF QSPHSBN DPOUFYUT UIBU DBO FMJNJOBUF BO JOUFHFS BSF EJTUJODU GSPN CPPMFBO QSPHSBN DPOUFYUT 'PS FYBNQMF BO JOUFHFS DPOUFYU NJHIU CF [·] + 3 XIFSF [·] JT B ۠IPMFۡ JOUP XIJDIBO JOUFHFS WBMVF DBO CF ੗MMFE CVU UIJT DPOUFYU DBO OFWFS CF DPOGVTFE XJUI BOZ CPPMFBO DPOUFYUTVDI BT if [·] then 𝑒 1 else 𝑒 2  य़FSFGPSF OP NB॒FS IPX B DPOUFYU VTFT UIF NFSHFE WBMVF JU JT VO
BNCJHVPVT XIFUIFS UIF 1 PS true NVTU CF QSPKFDUFE 'PS JOTUBODF XF IBWF (1 ! true) + 3 FWBMVBUFTUP 1 + 3
/PX DPOTJEFS UIF VOJPO UZQF Int % Bool 8F BTTVNF UIBU VOJPOT BSF VOUBHHFE NFBOJOH UIBU BU
SVOUJNF UIFSF JT OP FYUSB JOGPSNBUJPO BEEFE UP JOEJDBUF XIFUIFS B WBMVF PG UIJT UZQF IBT UIF UZQF
PO UIF MFॏ TJEF PS UIF SJHIU TJEF PG UIF VOJPO /FWFSUIFMFTT BT MPOH BT JOUFHFS BOE CPPMFBO WBMVFTIBWF EJTUJODU SVOUJNF SFQSFTFOUBUJPOT JF UIFZ IBWF TFQBSBUF DPOTUSVDUPST JU JT QPTTJCMF UP IBWF B
DPOTUSVDU UIBU DBO UFMM WBMVFT PG POF UZQF GSPN UIF PUIFS BT JO UIJT FYBNQMF GSPN UIF JOUSPEVDUJPO
match e with {(y : Bool) ↦→ false, (x : Int) ↦→ true}(JWFO UIBU FWFO XJUIPVU VOJPO UZQFT QB॒FSO NBUDIJOH PO CPPMFBO BOE JOUFHFS WBMVFT JT B TFOTJCMF PQFSBUJPO UIF CFIBWJPS PG UIF BCPWF NBUDI FYQSFTTJPO TIPVME CF OP TVSQSJTF *U JT BॏFS BMM
FRVJWBMFOU UP UIF MBSHF FYQSFTTJPO
match e with {true ↦→ false, false ↦→ false, 0 ↦→ true, −1 ↦→ true, 1 ↦→ true, . . .})PXFWFS OPX UIBU XF IBWF JOUSPEVDFE B TJOHMF FMJNJOBUJPO GPSN UIBU XPSLT PO UIF VOJPO UZQF
Int % Bool NFSHJOH CFDPNFT OPOEFUFSNJOJTUJD BT XF TBX JO UIF DBTF e = 1 ! true *O PUIFS XPSET
JO 𝜆𝑖 Int BOE Bool BSF OPU EJTUJOHVJTIBCMF CFDBVTF UIFSF JT OP DPOUFYU UIBU DBO UBLF B WBMVF UIBUJT FJUIFS BO Int PS Bool BOE EFUFSNJOF XIJDI UZQF PG WBMVF XBT QSPWJEFE "T B SFTVMU JU JT TBGF GPSUIFTF UZQFT UP CF NFSHFBCMF JO UIBU TF॒JOH 8JUI VOJPOT BOE UIFJS FMJNJOBUJPO GPSNT UIJT JT OP
MPOHFS UIF DBTF "MUIPVHI QFSNJ॒FE CZ 𝜆𝑖 NFSHFT MJLF 1 ! true BSF OPU SFRVJSFE GPS NBOZ QSBDUJDBMBQQMJDBUJPOT JODMVEJOH PVST य़VT JO F⊲⊳ XF QSFGFS UP DPOTJEFS Int BOE Bool EJTUJOHVJTIBCMF JOFYDIBOHF GPS TBDSJ੗DJOH UIF BCJMJUZ UP NFSHF UIFN*O DPOUSBTU UIF UZQF (Int → Bool)%(Bool → Bool) JT RVJUF EJ੖FSFOU 6OMJLF JOUFHFS BOE CPPMFBOWBMVFT GVODUJPOT HFOFSBMMZ EP OPU TVQQPSU QB॒FSO NBUDIJOH UIFZ BSF FMJNJOBUFE WJB BQQMJDBUJPOय़VT GSPN B UZQFUIFPSFUJD QPJOU PG WJFX B QSPHSBN MJLF
match e with {(x : Int → Bool) ↦→ true, (y : Bool → Bool) ↦→ false}
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

(1)

" #PXUJF GPS B #FBTU

JT VOVTVBM *U SFQSFTFOUT BO PQFSBUJPO PO B GVODUJPOۘPUIFS UIBO BQQMJDBUJPOۘUIBU QSPWJEFT JOGPSNBUJPO BCPVU XIJDI JOQVUT UIF GVODUJPO BDDFQUT 6OMJLF UIF QSFWJPVT FYBNQMF XJUI Int % Bool UIFSF
JT OP TJNJMBS XBZ UP FYQSFTT UIJT LJOE PG UZQFDBTF BOBMZTJT XJUI NPSF QSJNJUJWF QB॒FSOT*NQMFNFOUJOH TVDI B NBUDIJOH DPOTUSVDU XPVME SFRVJSF UIBU GVODUJPOBM WBMVFT BSF UBHHFE XJUIUZQF JOGPSNBUJPO BU SVOUJNF य़BOLT UP TVCUZQJOH UIF UZQF UBH PG B WBMVF DPVME OPU CF EJSFDUMZ DPNQBSFE XJUI UIF UZQF BOOPUBUJPO JO B QB॒FSO य़FSFGPSF SVOUJNF FYFDVUJPO PG UIF TVCUZQJOH BMHPSJUIN XPVME CF OFDFTTBSZ 4VDI BO BSSBOHFNFOU DFSUBJOMZ IBT QSFDFEFOU JO UIF MJUFSBUVSF <$BTUBHOBFU BM > BOE JO 001 MBOHVBHF JNQMFNFOUBUJPOT CVU F⊲⊳ BJNT UP JOUSPEVDF VOJPO UZQFT XJUIPVUDIBOHJOH UIF NFBOJOH PG FYJTUJOH UZQFT *O PUIFS XPSET TVQQPSU GPS VOJPO UZQFT TIPVME OPU EFQFOE
PO BEEJOH OFX PQFSBUJPOT PO UIF WBMVFT PG PUIFS UZQFT 0VS BQQSPBDI SFRVJSFT OFJUIFS BEEJUJPOBMUZQF UBHT BU SVOUJNF OPS BOZ UZQFUBH DPNQBSJTPO JO UIF EJTQBUDI QSPDFEVSF "T XF TIBMM TFF F⊲⊳
XJMM FYQMPJU UZQF BOOPUBUJPOT PO UIF NFSHF PQFSBUPS BU SVOUJNF CVU UIPTF BSF QBSU PG UIF NFSHF
DPOTUSVDUۘUIFZ BSF OPU QBSU PG UIF SFQSFTFOUBUJPO PG WBMVFT
0WFSMPBEJOH 0WFSMPBEJOH GBDFT UIF TBNF JTTVFT XJUI EFUFSNJOJTN BT QB॒FSO NBUDIJOH PO VOJPOT
8IFO UIF NFSHF PQFSBUPS PWFSMPBET GVODUJPOT XF DBO SFXSJUF UIF QSPCMFNBUJD FYBNQMF BT
((𝜆x : Int. true) ! (𝜆y : Bool. false)) (1 ! true)

य़F NFSHFE GVODUJPO DBO CF HJWFO UIF UZQF (Int → Bool) # (Bool → Bool) XIJDI EVF UP TVCUZQJOH JT FRVJWBMFOU UP (Int % Bool) → Bool 4FNBOUJDBMMZ UIFTF NFSHFE GVODUJPOT BDU MJLF UIF NBUDIFYQSFTTJPO UIBU XF BMSFBEZ TBXmatch e with {(x : Int) ↦→ true, (y : Bool) ↦→ false}*OEFFE GPS UIJT SFBTPO F⊲⊳ VOJ੗FT UIF TZOUBY GPS QB॒FSO NBUDI FYQSFTTJPOT XJUI UIF TZOUBY GPSQPUFOUJBMMZ NFSHFE MBNCEB BCTUSBDUJPOTۘUIFZ BSF UIF TBNF UIJOH*OGPSNBUJPO )JEJOH BOE 1BࣄFSO .BUDIJOH

0WFSMPBEFE 'VODUJPOT BOE $PQBࡇFSO .BUDIJOH " DPNNPO OPUBUJPO UP SFQSFTFOU PWFSMPBEFE GVODUJPOT JO DPSF DBMDVMJ JT XJUI 𝜆 BCTUSBDUJPOT DPOUBJOJOH B DBTF GPS FBDI PWFSMPBE TVDI BT
𝜆{((x : Int) ↩→ Bool) ↦→ true, ((x : Bool) ↩→ Bool) ↦→ false}(2)

य़JT JT UIF OPSNBMJ[FE GPSN PG UIF NFSHF XF TBX BCPWF *O FBDI DBTF UIF UZQF UP UIF SJHIU PG UIF↩→ JT UIF UZQF UIF GVODUJPO SFUVSOT XIFO UIBU DBTF JT NBUDIFEय़JT OPUBUJPO JT TJNJMBS UP ()$‫۝‬T .CODFC%CUG BOE 0$BNM‫۝‬T HWPEVKQP TZOUBY CPUI PG XIJDIDPNCJOF UIF JOUSPEVDUJPO PG B GVODUJPO XJUI QB॒FSO NBUDIJOH PO JUT BSHVNFOU *U NBZ BMTP CF TFFO
BT B GPSN PG DPQBࡇFSO NBUDIJOH <"CFM FU BM  ;FJMCFSHFS > BOE JT DPNNPO JO UIF MJUFSBUVSF
PO PWFSMPBEJOH <$BTUBHOB FU BM >
5ZQJDBM QB॒FSO NBUDIJOH JOWPMWFT EFTUSVDUVSJOH B WBMVF BDDPSEJOH UP B QB॒FSO EFTDSJCJOH UIFTIBQF PG BO JOUSPEVDUJPO GPSN *O FYBNQMF  PO UIF PUIFS IBOE UIF 𝜆WBMVF EFTUSVDUVSFT JUTFWBMVBUJPO DPOUFYU BDDPSEJOH UP FMJNJOBUJPO QBࡇFSOT JF DPQB॒FSOT UIBU EFTDSJCF UIF TIBQF PG
FMJNJOBUJPO GPSNT *O UIBU FYBNQMF UIF DPOUFYU [·] 1 NBUDIFT UIF ੗STU FMJNJOBUJPO QB॒FSO (x :Int) ↩→ Bool XIFSFBT UIF DPOUFYU [·] true NBUDIFT UIF TFDPOE *O UIJT XBZ EJTQBUDIۘUIF QSPDFTT PG EFDJEJOH XIJDI PWFSMPBE PG B GVODUJPO UP FYFDVUFۘJT DPNQMFUFMZ TVCTVNFE CZ DP QB॒FSONBUDIJOH𝜂&YQBOTJPO 3FDBMM UIF EF੗OJUJPO PG 𝑒 ! 
𝑒 ! = let x : {l2 : Bool} = {l1 ↦→ 1, l2 ↦→ true} in ({l1 ↦→ 2} ! x).l1 + 3

1SFWJPVTMZ XF TBX UIBU UIF FYQFDUFE TFNBOUJDT TIPVME IJEF UIF l1 ੗FME BU UIF BTTJHONFOU PG x 5ZQF
BOOPUBUJPOT PVHIU UP IBWF UIF F੖FDU BU SVOUJNF PG IJEJOH JOGPSNBUJPO TVDI BT B ੗FME PG B SFDPSE
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

/JDL 3JPVY 9VFKJOH )VBOH #SVOP $ E 4 0MJWFJSB BOE 4UFWF ;EBODFXJDPS BO PWFSMPBE PG B GVODUJPO JO B UFSN F⊲⊳ JNQMFNFOUT UIJT CZ 𝜂FYQBOEJOH BOOPUBUFE UFSNT "O
FYQSFTTJPO (v : {l2 : Bool}) 𝜂FYQBOET UP {l2 ↦→ (v.l2 : Bool)} IJEJOH BOZ JOGPSNBUJPO PUIFS UIBOUIF DPOUFOUT PG UIF ੗FME l2 UIBU NBZ CF QSFTFOU JO v
*O UIJT XBZ 𝜂FYQBOTJPO PG B WBMVF BU B UZQF CVJMET B XSBQQFS UIBU MJNJUT BDDFTT UP UIF WBMVF UP
UIF PQFSBUJPOT TVQQPSUFE CZ UIF UZQF य़JT UFDIOJRVF JT RVJUF TJNJMBS UP IPX TPVOE HSBEVBM UZQF
TZTUFNT <4JFL BOE 5BIB > CVJME XSBQQFST UP DBUDI SVOUJNF UZQF FSSPST DBVTFE CZ VOUZQFE DPEF
QBTTJOH JMMUZQFE WBMVFT UP UZQFE DPOUFYUT'PSNBMMZ JO F⊲⊳ B WBMVF v JOTJEF B XSBQQFS GPS UZQF A JT XSJ॒FO 𝜆{(∗ ↩→ A) ↦→ v} TP XF XPVMEXSJUF UIF FYBNQMF BCPWF BT 𝜆{(∗ ↩→ {l2 : Bool}) ↦→ v} )FSF UIF FMJNJOBUJPO QB॒FSO ∗ ↩→ A
NBUDIFT BOZ DPOUFYU WBMJE GPS UZQF A 8IFO UIJT PDDVST v JT QMBDFE JOTJEF UIJT DPOUFYU *O PUIFSXPSET UIF WBMVF 𝜆{(∗ ↩→ A) ↦→ v} CFIBWFT FYBDUMZ BT v CVU POMZ JO DPOUFYUT WBMJE GPS UZQF A य़F∗ QB॒FSO JT B TPSU PG EVBM UP WBSJBCMF QB॒FSOT

1BࡇFSO &YQBOTJPO JT 𝜂&YQBOTJPO 8F IBWF BMSFBEZ TFFO UIBU UZQF BOOPUBUJPOT PO QB॒FSO WBSJBCMFT IBWF TJHOJ੗DBODF BU SVOUJNF य़FJS NFBOJOH JT EFSJWFE GSPN 𝜂 QSJODJQBMT GPS QPTJUJWF UZQFT$POTJEFS BO F⊲⊳ FYQSFTTJPO MJLF match e with {(x : Bool) ↦→ e ( } %VBMMZ UP 𝜂 FYQBOTJPO GPS B WBMVFPG SFDPSE UZQF XIJDI SFCVJMET BO PVUQVU BOE QSPKFDUT FBDI ੗FME JOEJWJEVBMMZ 𝜂 FYQBOTJPO GPS B
QPTJUJWF UZQF MJLF Bool SFCVJMET BO JOQVU CZ NBUDIJOH BHBJOTU BMM QPTTJCMF WBMVFT PG B UZQF BOE
TQFDJBMJ[JOH FBDI CSBODI (JWFO UIF UFSN e ( BCPWF IBT B GSFF WBSJBCMF x : Bool UIF HFOFSBM GPSN PG
𝜂 FYQBOTJPO GPS CPPMFBOT XPVME CF
e ( →𝜂 match x with {true ↦→ e ( [true/x], false ↦→ e ( [false/x]}'SPN UIJT POF NJHIU JOGPSNBMMZ FYQFDU BO FRVJWBMFODF

match e with {(x : Bool) ↦→ e ( } ≡ match e with {true ↦→ e ( [true/x], false ↦→ e ( [false/x]}*O F⊲⊳ UIJT FYQBOTJPO JT OPU KVTU BO FRVJWBMFODF JU JT UIF EF੗OJUJPO PG UIF PQFSBUJPOBM TFNBOUJDT PG
QB॒FSO NBUDIJOH य़JT JT QPTTJCMF CFDBVTF TJNJMBS FYQBOTJPOT FYJTU GPS BMM QPTJUJWF UZQFT %VSJOHFMJNJOBUJPO QB॒FSO NBUDIJOH B EVBM LJOE PG FYQBOTJPO PDDVST GPS ∗QB॒FSOT य़F XSBQQFS 𝜆{(∗ ↩→{l2 : Bool}) ↦→ v} JT FRVJWBMFOU UP {l2 ↦→ (v.l2 : Bool)} *O PUIFS XPSET UIF QB॒FSO ∗ ↩→ 𝐴−𝜂FYQBOET BDDPSEJOH UP UIF OFHBUJWF UZQF 𝐴−  *O TVNNBSZ JO F⊲⊳ XF DBO DIBSBDUFSJ[F UIF UZQF
EJSFDUFE DPNQPOFOU PG UIF PQFSBUJPOBM TFNBOUJDT BT SVOUJNF 𝜂FYQBOTJPO$PNQPTJUJPOBM 1SPHSBNNJOH JO F⊲⊳

5P TFF IPX F⊲⊳ TVQQPSUT UIF LJOE PG OFTUFE DPNQPTJUJPOBM QSPHSBNNJOH P੖FSFE CZ UIF NFSHF
PQFSBUPS BOE UP JOUSPEVDF UIF OPUBUJPO VTFE CZ UIF DBMDVMVT XF OFYU DPOTJEFS IPX UP CVJME B
TNBMM FYUFOTJCMF JOUFSQSFUFS
*O F⊲⊳ XF DBO SFQSFTFOU B MBOHVBHF PG JOUFHFS MJUFSBMT BOE BEEJUJPO FYQSFTTJPOT CZ EF੗OJOH UIFUZQF IntArithExpr A BT B SFDPSE UZQF BTIntArithExpr A = {constant : Int → A, add : A → A → A}

य़JT UZQF SFQSFTFOUT B TJNQMJ੗FE GPSN PG B DPNQPTJUJPOBM JOUFSGBDF <;IBOH FU BM > BOE JTDMPTFMZ SFMBUFE UP UIF LJOE PG JOUFSGBDFT VTFE JO UFDIOJRVFT TVDI BT टOBMMZ UBHMFTT <$BSF॒F FU BM
> PS PCKFDU BMHFCSBT <0MJWFJSB BOE $PPL > *OEFFE UIJT JOUFSGBDF JT FTTFOUJBMMZ UIF GPME '"MHFCSB <#JSE BOE EF .PPS > GPS B TJNQMF EBUBUZQF PG BSJUINFUJD FYQSFTTJPOT "O F⊲⊳ UFSN PG
UZQF IntArithExpr A EFTDSJCFT IPX UP JOUFSQSFU BO FYQSFTTJPO JO PVS PCKFDU MBOHVBHF BT B WBMVF PG
UZQF A 8F SFQSFTFOU POF TVDI PCKFDUMBOHVBHF FYQSFTTJPO BT GPMMPXT
three : ∀ 𝛼 .IntArithExpr 𝛼 → 𝛼three = Λ𝛼 .𝜆(x : IntArithExpr 𝛼) ↩→ 𝛼 . x.add (x.constant 1) (x.constant 2)
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

" #PXUJF GPS B #FBTUय़F OPUBUJPO Λ𝛼 .e CJOET B UZQF WBSJBCMF 𝛼 JO UIF CPEZ e XIJMF 𝜆(x : B) ↩→ C. e CJOET UIF UFSNWBSJBCMF x PG UZQF B JO UIF CPEZ e XIJDI JT BTDSJCFE UIF UZQF C 7BMVFT TVDI BT three BSF EF੗OFECZ JNQMFNFOUJOH UIFJS GPMET" OBUVSBM XBZ PG JOUFSQSFUJOH PCKFDUMBOHVBHF FYQSFTTJPOT BT JOUFHFST JT CZ FWBMVBUJOH UIFNय़F JOUFSQSFUBUJPO evalInt EFTDSJCFT IPX UP EP UIJT CZ EF੗OJOH B NFBOJOH GPS FBDI ੗FME
evalInt : IntArithExpr Int
evalInt = {constant ↦→ 𝜆x : Int ↩→ Int. x, add ↦→ (+)}/PX UIF QSPHSBN three [Int] evalInt PG UZQF Int FWBMVBUFT UP 3
4VQQPTF UIBU XF XJTI UP FYUFOE UIJT MBOHVBHF TP UIBU B DPOTUBOU NBZ CF FJUIFS BO JOUFHFS PS
B ੘PBUJOH QPJOU OVNCFS 'PS TJNQMJDJUZ XF XJMM OPU QSFTVNF BOZ TVCUZQJOH SFMBUJPOTIJQ CFUXFFOInt BOE Float CVU JOTUFBE SFMZ PO BO FYQMJDJU DBTU toFloat : Int → Float 8IBU XF XJTI JT UP PC
UBJO B DPNCJOFE MBOHVBHF XIFSF CPUI ੘PBUJOH QPJOU OVNCFST BOE JOUFHFST DBO CF VTFE .PSFPWFSUIF MBOHVBHF TIPVME BVUPNBUJDBMMZ DPOWFSU CFUXFFO JOUFHFST BOE ੘PBUJOH QPJOU OVNCFST XIFOOFDFTTBSZ 0SDIBSE BOE 4DISJKWFST <> UBDLMF B TJNJMBS QSPCMFN JO UIF TF॒JOH PG B UZQFE PCKFDUMBOHVBHF य़FZ JMMVTUSBUF UIBU UIF QSPCMFN JT USJDLZ UP TPMWF JO )BTLFMM VTJOH B ੗OBMMZ UBHMFTT FNCFEEJOH 5P UIJT FOE 0SDIBSE BOE 4DISJKWFST QSPQPTFE UP FYUFOE )BTLFMM XJUI DPOTUSBJOU TZOPOZNTXIJDI MBUFS IFMQFE NPUJWBUF UIF BEEJUJPO PG UIF %QPUVTCKPV-KPFU ()$ FYUFOTJPO *O DPOUSBTU JO
F⊲⊳ NFSHFCBTFE PWFSMPBEJOH XJUI JOUFSTFDUJPO BOE VOJPO UZQFT QSPWJEFT XIBU XF OFFE
8F EF੗OF UIF UZQF IntFloatArithExpr A BT BO FYUFOTJPO PG IntArithExpr A VTJOH JOUFSTFDUJPO
0CTFSWF UIBU UIF JOUFSTFDUJPO EJTUSJCVUFT PWFS UIF SFDPSE BVHNFOUJOH UIF UZQF PG UIF constant ੗FME
IntFloatArithExpr A = IntArithExpr A # {constant : Float → A}
≡ {constant : (Int → A) # (Float → A), add : A → A → A}
≡ {constant : Int % Float → A, add : A → A → A}

*O PUIFS XPSET TVCUZQJOH HJWFT VT UIF FRVJWBMFODF (Int → A) # (Float → A) ≡ (Int % Float) → A
4VDI FRVJWBMFODFT BSF LFZ UP DPNQPTJUJPOBM QSPHSBNNJOH <#J FU BM >
5P FWBMVBUF FYQSFTTJPOT JO UIJT MBOHVBHF XF OFFE UP EF੗OF BO JOUFSQSFUBUJPO evalIntFloat :IntFloatArithExpr (Int % Float) " ੗STU TUFQ JT UP EF੗OF UIF UZQF FYQSFTTJPOT BT XFMM BT UIF FWBMVBUJPO GVODUJPO GPS UIF TVCMBOHVBHF DPOUBJOJOH ੘PBUJOH QPJOU CVU OPU JOUFHFS MJUFSBMT 8F VTF +.
GPS UIF ੘PBUJOHQPJOU BEEJUJPO QSJNJUJWF
FloatArithExpr A = {constant : Float → A, add : A → A → A}
evalFloat : FloatArithExpr Float
evalFloat = {constant ↦→ 𝜆x : Float ↩→ Float. x, add ↦→ (+.)}*U JT OPX QPTTJCMF UP NFSHF PVS UXP FWBMVBUPST

partialEvalIntFloat : (IntArithExpr Int) # (FloatArithExpr Float)
partialEvalIntFloat = evalInt ! evalFloat#VU XF BSF OPU ੗OJTIFE XF XPVME MJLF BO FYQSFTTJPO PG UZQF IntFloatArithExpr (Int % Float) CVU
POMZ IBWF POF PG UZQF (IntArithExpr Int) # (FloatArithExpr Float) य़JT JT OPU FOPVHI CFDBVTF UIFGPSNFS UZQF SFRVJSFT UIF add PQFSBUJPO UP TVQQPSU BEEJUJPO PG JOUFHFST XJUI ੘PBUJOH QPJOU OVNCFSTXIJDI UIF MB॒FS EPFT OPU "T B SFTVMU USZJOH UP VTF partialEvalIntFloat UP FWBMVBUF four EF੗OFE
CFMPX XPVME CF JMM UZQFE
four = Λ𝛼 .𝜆(x : IntFloatArithExpr 𝛼) ↩→ 𝛼 .
x.add (x.constant 2.0) (x.constant 2)
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

/JDL 3JPVY 9VFKJOH )VBOH #SVOP $ E 4 0MJWFJSB BOE 4UFWF ;EBODFXJDFYQSFTTJPOTe::=WBMVFTv::=

WBMVF QBࡇFSOTp::=

FMJN GSBNFT
FMJN QBࡇFSOT

F
𝑝ˆ

::=
::=

x | c e | e1 e2 | e [A]| (e : A)| (e1 : A1 ) ! (e2 : A2 )| 𝜆{𝑝ˆ1 ↦→ e1, ... , 𝑝ˆn ↦→ en }x | cv| 𝜆{𝑝ˆ1 ↦→ e1, ... , 𝑝ˆn ↦→ en }x : A | c 𝑝 | (𝑝 1 |𝑝 2 )| 𝑝 1 &𝑝 2

UZQFT

A, B, C::=

OFH UZQFT

𝐴− , 𝐵 −::=FMJN UZQFT

ˆ 𝐵ˆ
𝐴,

::=

A | [A]

Γ, Δ::=· | Γ, 𝛼 | Γ, x : A[·]v | [·] [A]FOWJSPONFOUT∗ ↩→ 𝐴− | p ↩→ B | 𝛼 ↩→ B

𝛼 | cA| A → B | ∀ 𝛼 .B
| ⊥ | A1 % A2
| , | A1 # A2
A → B | ∀ 𝛼 .B−
| 𝐴−
1 % 𝐴2−| , | 𝐴1 # 𝐴−
2

'JH  F⊲⊳ 4ZOUBY*O PSEFS UP DPNQMFUF UIF FWBMVBUPS XF OFFE BO BEEJUJPO FYUFOTJPO UIBU IBOEMFT UIF NJTTJOH DBTFT*UT UZQF JT HJWFO CFMPXArithExt = {add : (Int → Float → Float) # (Float → Int → Float)}

8F JNQMFNFOU UIF FYUFOTJPO CZ DPFSDJOH JOUFHFST UP ੘PBUT BOE VTJOH ੘PBUJOH QPJOU BEEJUJPO BT
TIPXO JO UIF DPEF CFMPX /PUF UIBU UIF add ੗FME PG UIF SFDPSE DPOUBJOT B ۠GVODUJPOۡ XJUI UXPCPEJFT EJTUJOHVJTIFE CZ UIF JOQVU UZQF PG UIF BSHVNFOU x
evalExt : ArithExt
evalExt = {add ↦→ 𝜆{ (x : Int) ↦→ 𝜆(y : Float) ↩→ Float. toFloat x +. y,(x : Float) ↦→ 𝜆(y : Int) ↩→ Float. x +. toFloat y } }"QQMZJOH EJTUSJCVUJWJUZ XF DBO TIPX UIBU(IntArithExpr Int) # (FloatArithExpr Float) # ArithExt ≤ IntFloatArithExpr (Int % Float)

य़JT UFMMT VT UIBU NFSHJOH partialEvalIntFloat XJUI evalExt ZJFMET BO FYQSFTTJPO PG UIF EFTJSFE UZQF
evalIntFloat : IntFloatArithExpr (Int % Float)
evalIntFloat = partialEvalIntFloat ! evalExt/PX FWBMVBUJOH four [Int % Float] evalIntFloat SFTVMUT JO UIF ੘PBUJOHQPJOU WBMVF 4.0 BT FYQFDUFE

4:45&. F⊲⊳

8F XJMM OPX NBLF UIF JOUVJUJPOT GSPN FBSMJFS QSFDJTF य़JT TFDUJPO QSFTFOUT UIF TZOUBY BOE PQFSBUJPOBM TFNBOUJDT PG F⊲⊳ JO GVMM


4ZOUBY&YQSFTTJPOT 'JHVSF  QSFTFOUT UIF TZOUBY PG F⊲⊳  &YQSFTTJPOT JODMVEF TUBOEBSE TZOUBY TVDI BT WBSJBCMFT BQQMJDBUJPO PG GVODUJPOT UP BSHVNFOUT BOE BQQMJDBUJPO PG UFSNT UP UZQFT "O VOEFSTDPSF JT
VTFE JO QMBDF PG B WBSJBCMF OBNF XIFO UIF WBSJBCMF JT OFWFS SFGFSFODFE य़F c e GPSN UBHT UIF FYQSFTTJPO e XJUI DPOTUSVDUPS c य़F DPOTUSVDUPS c DPNFT GSPN TPNF QSFEFUFSNJOFE TFU PG TZNCPMTUIF NFUBWBSJBCMFT l BOE k BMTP SBOHF PWFS UIJT TFU QBSUJDVMBSMZ XIFO UIF DPOTUSVDUPS SFQSFTFOUT B
SFDPSE MBCFM य़F OPUBUJPO (e : A) ! (e ( : B) EFOPUFT B NFSHF PG UXP UZQFBOOPUBUFE FYQSFTTJPOT
8F EFOPUF B TVCTFU PG FYQSFTTJPOT BT WBMVFT WBSJBCMFT DPOTUSVDUPST XJUI WBMVFT BT BSHVNFOUT
BOE 𝜆 GPSNT 8F BMTP EFTDSJCF FMJNJOBUJPO GSBNFT XIJDI BSF DPOUFYUT JO UIF TIBQF PG BO FMJNJOBUJPOGPSN XJUI B IPMF JO IFBE QPTJUJPO &MJNJOBUJPO GSBNFT QMBZ B SPMF EVBM UP UIBU PG WBMVFT JO QB॒FSONBUDIJOH
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

" #PXUJF GPS B #FBTU

A + B = left A % right B
Bool = , + ,{l : A} = l , → A{l1 : A1, ... , ln : An } = {l1 : A1 } # ... # {ln : An }true = left 𝜆{ }false = right 𝜆{ }𝜆x : A. e = 𝜆{x : A ↦→ e}e.l = e (l 𝜆{ })Λ𝛼 .e = 𝜆{𝛼 ↦→ e}{l1 ↦→ e1, ... , ln ↦→ en } = 𝜆{(@ : l1 ,) ↦→ e1, ... , (@ : ln ,) ↦→ en }match e with {𝑝 1 ↦→ e1, ... , 𝑝 n ↦→ en } = 𝜆{𝑝 1 ↦→ e1, ... , 𝑝 n ↦→ en } e'JH  6TFGVM "CCSFWJBUJPOT5ZQFT य़F UZQFT PG F⊲⊳ JODMVEF UZQF WBSJBCMFT 𝛼 DPOTUSVDUPST BQQMJFE UP BO BSHVNFOU c A GVODUJPOTA → B BOE VOJWFSTBM RVBOUJ੗FST ∀ 𝛼 .B "EEJUJPOBMMZ UIF ⊥ UZQF JT VOJOIBCJUFE XIJMF , JT JOIBCJUFECZ UIF USJWJBM WBMVF 𝜆{ } 'JOBMMZ F⊲⊳ UZQFT JODMVEF VOJPOT A % B BOE JOUFSTFDUJPOT A # B 8F
TPNFUJNFT XSJUF 𝑛BSZ JOUFSTFDUJPOT BOE VOJPOT TVDI BT A1 # ... # An  य़JT OPUBUJPO EPFT OPU
QSFDMVEF UIF QPTTJCJMJUZ UIBU n = 0 JO XIJDI DBTF UIF UZQF JT , PS ⊥ JO UIF DBTF PG 0BSZ VOJPOT 
8F XJMM JO g JOUSPEVDF TPNF SFTUSJDUJPOT PO XIJDI VOJPOT BOE JOUFSTFDUJPOT BSF DPOTJEFSFE UP
CF XFMMGPSNFE/FHBUJWF UZQFT BSF UIPTF UIBU BSF JOUSPEVDFE CZ 𝜆 BOE FMJNJOBUFE XJUI TUSPOH OPONBUDIJOHFMJNJOBUJPO GPSNT य़FTF JODMVEF GVODUJPOT RVBOUJ੗FST , BOE VOJPOT BOE JOUFSTFDUJPOT PG OFHBUJWFUZQFT &MJNJOBUJPO UZQFT BSF BTTPDJBUFE XJUI FMJNJOBUJPO GPSNT "O FMJNJOBUJPO UZQF 𝐴ˆ = A DPSSF
TQPOET UP BO BQQMJDBUJPO [·] e JO XIJDI UIF BSHVNFOU e IBT UZQF A UIF FMJNJOBUJPO UZQF 𝐴ˆ = [A]DPSSFTQPOET UP B QPMZNPSQIJD JOTUBOUJBUJPO [·] [A]य़F UZQJOH BMHPSJUIN NBLFT VTF PG VOPSEFSFE FOWJSPONFOUT Γ XIJDI CPUI DPOUBJO UZQF WBSJBCMFT
BOE NBQ UFSN WBSJBCMFT UP UIFJS UZQFT य़F UZQF BTTPDJBUFE XJUI B UFSN WBSJBCMF JO BO FOWJSPONFOUΓ NBZ SFGFSFODF BOZ GSFF UZQF WBSJBCMF JO Γ
&ODPEJOHT 7BSJPVT TUBOEBSE TZOUBY DBO CF FODPEFE JO UFSNT PG F⊲⊳ ‫۝‬T DPOTUSVDUT 'PS FYBNQMF POF
NJHIU JO UIFPSZ FODPEF Int UIF UZQF PG CJU JOUFHFST BT B VOJPO PG 232 EJTUJODU DPOTUSVDUPST'JHVSF  DPOUBJOT PUIFS VTFGVM BCCSFWJBUJPOT य़JT ੗HVSF PNJUT BT XF PॏFO EP SFUVSO UZQF BOOPUBUJPOT ↩→ A XIFSF UIFZ BSF UP CF JOGFSSFE GSPN DPOUFYU 4VN UZQFT BSF SFQSFTFOUFE CZ VOJPOT PG UIFQSFTVNFEEJTUJODU left BOE right DPOTUSVDUPST 3FDPSE UZQFT BSF BMTP FODPEBCMF BT GVODUJPOT GSPN੗FME MBCFMT UP UIF DPSSFTQPOEJOH WBMVF य़F UZQF PG B MBCFM JT SFQSFTFOUFE BT l , UIF DPOTUSVDUPSl XJUI B EVNNZ BSHVNFOU PG UZQF ,  " TJOHMF੗FME SFDPSE JT B GVODUJPO BDDFQUJOH POMZ UIF MBCFM
l 𝜆{ } BT JOQVU

1B࢔FSOT 1B॒FSO NBUDIJOH JT B EJTUJOHVJTIJOH GFBUVSF PG F⊲⊳  य़FSF BSF UXP UZQFT PG QB॒FSOT य़F
NFUBWBSJBCMF 𝑝 SBOHFT PWFS WBMVF QBࡇFSOT XIJDI BSF FTTFOUJBMMZ UIF QB॒FSOT PG )BTLFMM PS .- *O
B NBUDI DPOTUSVDU match v with {p1 ↦→ e1, ... , pn ↦→ en } UIF EJTDSJNJOFF v XJMM CF EFDPOTUSVDUFECZ UIF QB॒FSOT PG FBDI pi ↦→ ei DMBVTF
"T XF IBWF TFFO UIF 𝜆 GPSN DPOUBJOT B OVNCFS PG PWFSMPBEFE JNQMFNFOUBUJPOT PG B DPNQVUBUJPOXJUI UIF DPSSFDU POF DIPTFO EZOBNJDBMMZ CBTFE PO IPX UIF WBMVF JT VTFE CZ JUT DPOUFYU &BDIPWFSMPBE JT SFQSFTFOUFE BT B DMBVTF 𝑝ˆ ↦→ e XIFSF 𝑝ˆ JT BO FMJNJOBUJPO QB॒FSO PS DPQB॒FSO <"CFM
FU BM  ;FJMCFSHFS >  8F DBO UIJOL PG 𝜆 BT VTJOH UIFTF QB॒FSOT UP CVJME B DPNQVUBUJPO CZ
EFDPOTUSVDUJOH JUT JNNFEJBUF DPOUFYUۘTQFDJ੗DBMMZ UIF FMJNJOBUJPO GSBNF F 'PS FYBNQMF DPOTJEFSUIF GPMMPXJOH WBMVF
𝜆{((x : A1 ) ↩→ B1 ) ↦→ e1, ((x : A2 ) ↩→ B2 ) ↦→ e2, (𝛼 ↩→ B3 ) ↦→ e3 }*O B GSBNF PG TIBQF [·] v ( UIF e1 PS e2 PWFSMPBET BSF TFMFDUFE XIFO v ( IBT UZQF A1 PS A2 SFTQFDUJWFMZ*O GBDU CPUI NBZ CF CF TFMFDUFE BOE NFSHFE UPHFUIFS JG A1 BOE A2 BSF OPU EJTUJOHVJTIBCMF *O B
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

𝑀
E/JDL 3JPVY 9VFKJOH )VBOH #SVOP $ E 4 0MJWFJSB BOE 4UFWF ;EBODFXJD

::=
::=

{𝑝ˆ1 ↦→ e1, ... , 𝑝ˆn ↦→ en }[·] | c E | E e | v E | E[A]
| (E : A) | (E : A) ! (e : B)
| (v : A) ! (E : B)e ↦−→ e (TNBMMTUFQ SFEVDUJPOe ↦−→ e (E[e] ↦−→ E[e ( ]F [𝜆𝑀] ↦−→ disp(𝑀, F)(v : A) ↦−→ v−−−(v1 : 𝐴−1 ) ! (v2 : 𝐴2 ) ↦−→ 𝜆{∗ ↩→ 𝐴1 ↦→ v1 , ∗ ↩→ 𝐴2 ↦→ v2 }disp(𝑀, F) =!

𝑝ˆ ↦→ e ∈ 𝑀
F/𝑝ˆ ⇒ 𝜎 ↩→ B

(𝜎 (e) : B)

'JH  F⊲⊳ 0QFSBUJPOBM 4FNBOUJDT BOE "VYJMJBSZ %FGJOJUJPOTDPOUFYU PG TIBQF [·] [A] UIF UIJSE DMBVTF JT NBUDIFE JOTUFBE &BDI Bi JO UIF WBMVF JT BO PVUQVU UZQF
BOOPUBUJPO UIBU EFTDSJCFT UIF UZQF PG UIF DPSSFTQPOEJOH FYQSFTTJPO ei  /PUF UIBU 𝛼 JT CPVOE JO B3 
" DMBVTF (∗ ↩→ 𝐴− ) ↦→ v NBUDIFT BOZ FMJNJOBUJPO F UIBU JT WBMJE GPS B WBMVF PG UZQF 𝐴−  य़F
FMJNJOBUJPO GSBNF F UIFO CFDPNFT UIF DPOUFYU GPS v *O UIJT XBZ UIF FMJNJOBUJPO QB॒FSO ∗ JT B TPSUPG ۠QB॒FSO WBSJBCMFۡ UIBU QMBDFT UIF DVSSFOU DPOUFYU BSPVOE UIF FYQSFTTJPO JO XIJDI ∗ JT ۠CPVOEۡय़F QPJOU JT QVSFMZ UP FOGPSDF UIBU v IBT QSFDJTFMZ UIF UZQF 𝐴−  य़JT NBZ TFFN VOVTVBM CVU UIFTFNBOUJDT BSF TUSBJHIUGPSXBSE " UFSN 𝜆{(∗ ↩→ {l1 : A1 }) ↦→ {l1 ↦→ e1, l2 ↦→ e2 }} TIPVME CFUIPVHIU PG BT B XSBQQFS BSPVOE {l1 ↦→ e1, l2 ↦→ e2 } UIBU FOGPSDFT UIF UZQF {l1 : A1 } CZ IJEJOH UIF੗FME l2 "T XF IBWF TFFO UIJT IJEJOH JT BDIJFWFE VTJOH 𝜂FYQBOTJPO *O PUIFS XPSET XF BSF UBLJOH BE
WBOUBHF PG UIF GBDU UIBU 𝜆{(∗ ↩→ {l1 : A}) ↦→ v} JT FRVJWBMFOU UP 𝜆{(x : l1 ,) ↩→ A ↦→ v.l1 } य़JT
FYQMBJOT XIZ 𝐴− NVTU CF B OFHBUJWF UZQF POMZ OFHBUJWF UZQFT IBWF NPSF QSJNJUJWF FMJNJOBUJPOQB॒FSOT UP JOUSPEVDF UIFN XJUI य़F TZOUBY PG WBMVF QB॒FSOT BMTP JODMVEFT PS BOE BOEQB॒FSOT
XSJ॒FO p1 |p2 BOE p1 &p2  य़FTF QSPWJEF 𝜂QSJODJQMFT GPS VOJPO BOE JOUFSTFDUJPO UZQFT 7BSJBCMFT JOQB॒FSOT BSF BOOPUBUFE XJUI UIF UZQF PG WBMVF UIFZ BSF FYQFDUFE UP NBUDI य़FZ BSF CPVOE JO UIFSJHIU IBOE TJEF PG B DMBVTF


0QFSBUJPOBM 4FNBOUJDT" TNBMMTUFQ DBMMCZWBMVF PQFSBUJPOBM TFNBOUJDT JT HJWFO JO 'JHVSF  8F VTF 𝑀 UP SBOHF PWFS𝜆CPEJFT BOE E UP SBOHF PWFS FWBMVBUJPO DPOUFYUT &WBMVBUJPO QSPDFFET VOEFS BMM FWBMVBUJPO DPOUFYUT BT JT TUBOEBSE य़F NFUBWBSJBCMF 𝜎 SBOHFT PWFS TVCTUJUVUJPOT NBQQJOHT GSPN UFSN BOE UZQF
WBSJBCMFT UP WBMVFT BOE UZQFT " TVCTUJUVUJPO NBZ BMTP DPOUBJO BU NPTU POF TQFDJBM NBQQJOH GSPN ∗UP BO FMJNJOBUJPO GSBNF य़F OPUBUJPO 𝜎 (e) BQQMJFT UIF TVCTUJUVUJPO FWFSZ WBSJBCMF JO UIF EPNBJO
PG 𝜎 JT SFQMBDFE XJUI UIF DPSSFTQPOEJOH UZQF PS WBMVF JO e य़F SFTVMU JT UIFO QMBDFE JO UIF GSBNF F
JG TVDI B GSBNF FYJTUT JO 𝜎य़F VTVBM 𝛽 SVMFT GPS UZQF BOE UFSN BQQMJDBUJPO BSF TVCTVNFE JOUP B TJOHMF SVMF XIJDI FWBMVBUFTUFSNT PG UIF GPSN F [𝜆𝑀] TUSPOH FMJNJOBUJPO GPSNT BQQMJFE UP B WBMVF VTJOH UIF EJTQBUDI NFUBˆGVODUJPO disp य़JT QSPDFEVSF MPPLT BU FWFSZ DBTF 𝑝ˆ ↦→ e JO 𝑀 BOE DIFDLT XIFUIFS F NBUDIFT 𝑝
*G TP B TVCTUJUVUJPO 𝜎 BOE PVUQVU UZQF B BSF PCUBJOFE य़F SFTVMU PG disp JT UIFO B NFSHF PG UIFFYQSFTTJPO e PG FWFSZ NBUDIJOH DBTF XJUI BO BQQSPQSJBUF TVCTUJUVUJPO BQQMJFE GPS QB॒FSO WBSJBCMFTय़F OPUBUJPO F/𝑝ˆ ⇒ 𝜎 ↩→ B VTFE IFSF JOEJDBUFT UIBU FMJNJOBUJPO GSBNF F NBUDIFT FMJNJOBUJPOˆ XF XJMM TIPSUMZ QSFTFOU UIJT QSPDFTT JO NPSF EFUBJM " NFSHF PG UXP WBMVFT FWBMVBUFT UP B
QB॒FSO 𝑝𝜆FYQSFTTJPO XJUI UXP DPSSFTQPOEJOH DBTFT /PUF UIBU UIF UZQF UIBU FBDI PG UIF WBMVFT JT BOOPUBUFEXJUI JT SFNFNCFSFE UIF 𝜆 BDUT BT B XSBQQFS UP IJEF BDDFTT UP BOZ QBSU PG FJUIFS WBMVF OPU EFTDSJCFECZ JUT UZQF BOOPUBUJPO 5ZQF BOOPUBUJPOT PO FYQSFTTJPOT PUIFS UIBO NFSHFT DBO CF TBGFMZ ESPQQFEEVSJOH FWBMVBUJPO TJODF JG UIF FYQSFTTJPO HFUT NFSHFE JU XJMM CF BOOPUBUFE BHBJO JO UIF NFSHF
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

" #PXUJF GPS B #FBTU

WBMVF QBࡇFSO NBUDIJOH

v/p ⇒ 𝜎v/𝑝 ⇒ 𝜎v/𝑝 1 ⇒ 𝜎c v/c 𝑝 ⇒ 𝜎v/𝑝 2 ⇒ 𝜎v/(𝑝 1 |𝑝 2 ) ⇒ 𝜎

v/𝑝 1 ⇒ 𝜎1v/(𝑝 1 |𝑝 2 ) ⇒ 𝜎v/(𝑝 1 &𝑝 2 ) ⇒ 𝜎

𝜎 = 𝜎1 # 𝜎2v/c (x : A) ⇒ [x ↦→ v ( ]v/((x : A1 )& (x : A2 )) ⇒ 𝜎v/(x : 𝐴− ) ⇒ [x ↦→ v]

v/𝑝 2 ⇒ 𝜎2v/(x : c A) ⇒ [x ↦→ c v ( ]v/(x : A1 # A2 ) ⇒ 𝜎v/((x : A1 )| (x : A2 )) ⇒ 𝜎v/(x : A1 % A2 ) ⇒ 𝜎F/𝑝ˆ ⇒ 𝜎 ↩→ B

FMJNJOBUJPO QBࡇFSO NBUDIJOH
v/p ⇒ 𝜎[·]v/(p ↩→ B) ⇒ 𝜎 ↩→ B[·] [A]/(𝛼 ↩→ B) ⇒ [𝛼 ↦→ A] ↩→ B[A/𝛼]F/((x : A) ↩→ B) ⇒ [x ↦→ v] ↩→ B (F/(𝛼 ↩→ B) ⇒ [𝛼 ↦→ A ( ] ↩→ B (F/(∗ ↩→ (A → B)) ⇒ [ ∗ ↦→ [·]v] ↩→ B (F/(∗ ↩→ ∀ 𝛼 .B) ⇒ [ ∗ ↦→ [·] [A ( ]] ↩→ B (F/(∗ ↩→ 𝐴−1 ) ⇒ 𝜎1 ↩→ B1−
F/(∗ ↩→ 𝐴2 ) ⇒ 𝜎2 ↩→ B2
𝜎 = 𝜎1 # 𝜎2F/(∗ ↩→ 𝐴−1 ) ⇒ 𝜎1 ↩→ B1−
F/(∗ ↩→ 𝐴2 ) ⇒ 𝜎2 ↩→ B2
𝜎 = 𝜎1 % 𝜎2−F/(∗ ↩→ 𝐴−
1 % 𝐴2 ) ⇒ 𝜎 ↩→ B1 % B2

F/(∗ ↩→ 𝐴−1 ) ⇒ 𝜎 ↩→ B

F/(∗ ↩→ 𝐴−2) "−F/(∗ ↩→ 𝐴−
1 # 𝐴2 ) ⇒ 𝜎 ↩→ B

𝜎 = 𝜎1 # 𝜎2−F/(∗ ↩→ 𝐴−
1 # 𝐴2 ) ⇒ 𝜎 ↩→ B1 # B2

F/(∗ ↩→ 𝐴−1) "(𝜎1 # 𝜎2 )(𝛼)(𝜎1 # 𝜎2 )(𝛼)(𝜎1 # 𝜎2 )(𝛼)

=
=
=

A1
A2
A

XIFSF 𝜎1 (𝛼) = A1 BOE 𝛼 OPU JO 𝜎2
XIFSF 𝜎2 (𝛼) = A2 BOE 𝛼 OPU JO 𝜎1
XIFSF 𝜎1 (𝛼) = 𝜎2 (𝛼) = A(𝜎1 # 𝜎2 )(x)(𝜎1 # 𝜎2 )(x)(𝜎1 # 𝜎2 )(x)

=
=
=

v1
v2
v

XIFSF 𝜎1 (x) = v1 BOE x OPU JO 𝜎2
XIFSF 𝜎2 (x) = v2 BOE x OPU JO 𝜎1
XIFSF 𝜎1 (x) = 𝜎2 (x) = v(𝜎1 # 𝜎2 )(∗)
(𝜎1 # 𝜎2 )(∗)
(𝜎1 # 𝜎2 )(∗)

=
=
=

F1
F2
F

XIFSF 𝜎1 ( ∗ ) = F1 BOE ∗ OPU JO 𝜎2
XIFSF 𝜎2 ( ∗ ) = F2 BOE ∗ OPU JO 𝜎1
XIFSF 𝜎1 (∗) = 𝜎2 (∗) = F

F/(∗ ↩→ 𝐴−2 ) ⇒ 𝜎 ↩→ B−
F/(∗ ↩→ 𝐴−
1 # 𝐴2 ) ⇒ 𝜎 ↩→ B

𝜎 = 𝜎1 % 𝜎2
(𝜎1 % 𝜎2 ) (𝛼)=(𝜎1 % 𝜎2 ) (x)=(𝜎1 % 𝜎2 ) (∗)=

A
XIFSF 𝜎1 (𝛼) = 𝜎2 (𝛼) = Av
XIFSF 𝜎1 (x) = 𝜎2 (x) = v
F
XIFSF 𝜎1 (∗) = 𝜎2 (∗) = F'JH  1BࡻFSO .BUDIJOH

1BࡇFSO .BUDIJOH 'JHVSF  HJWFT UIF QB॒FSO NBUDIJOH BMHPSJUIN 8F XSJUF v/p ⇒ 𝜎 UP NFBOUIF WBMVF v NBUDIFT UIF WBMVF QB॒FSO p XIFSF 𝜎 EFTDSJCFT UIF DPSSFTQPOEJOH CJOEJOHT GPS QB॒FSO
WBSJBCMFT %VSJOH UIF NBUDIJOH QSPDFTT DPOTUSVDUPST BSF DPNQBSFE UP B QB॒FSO TUSVDUVSBMMZ 0S
QB॒FSOT NBUDI B WBMVF XIFO FJUIFS POF PG UIF UXP DPNQPOFOU QB॒FSOT NBUDI य़F UZQF TZTUFNXJMM FOTVSF UIBU UIF UXP QB॒FSOT BSF NVUVBMMZ FYDMVTJWF TP UIFSF JT OP OFFE GPS B SVMF UIBU IBOEMFT
CPUI QB॒FSOT NBUDIJOH "O BOEQB॒FSO NBUDIFT B WBMVF XIFO CPUI PG JUT TVCQB॒FSOT NBUDI य़F
SFTVMUT PG UIF UXP NBUDIFT BSF DPNCJOFE XJUI UIF QBSUJBM 𝜎1 # 𝜎2 PQFSBUJPO 0O TVCTUJUVUJPOT XJUIEJTKPJOU EPNBJOT UIJT PQFSBUJPO JT DPODBUFOBUJPO )PXFWFS XIFO UIF EPNBJOT PWFSMBQ JU JT EF੗OFE
POMZ XIFO BOZ WBSJBCMFT QSFTFOU JO CPUI SFTVMUT BSF BTTJHOFE UIF TBNF WBMVF
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

/JDL 3JPVY 9VFKJOH )VBOH #SVOP $ E 4 0MJWFJSB BOE 4UFWF ;EBODFXJD

7BSJBCMF QB॒FSOT BOOPUBUFE XJUI OFHBUJWF UZQFT USJWJBMMZ NBUDI BOZ WBMVF CFDBVTF WBMVFT PG
OFHBUJWF UZQF IBWF OP EJTDFSOJOH UBHT UP UBLF BEWBOUBHF PG JO UIF QB॒FSO NBUDIJOH QSPDFTT 0O
UIF PUIFS IBOE XIFO UIF UZQF JT QPTJUJWF XF DBO QFSGPSN 𝜂FYQBOTJPO य़F MBTU UISFF DBTFT PG UIFWBMVF QB॒FSO NBUDIJOH EF੗OJUJPO EF੗OF NBUDIJOH PG B WBSJBCMF QB॒FSO JO UFSNT PG QB॒FSOT GPS
UIF DPSSFTQPOEJOH UZQF *O UIJT XBZ UIFTF WBSJBCMF QB॒FSOT BSF FTTFOUJBMMZ KVTU TIPSUDVUT GPS NPSFQSJNJUJWF QB॒FSOT" WBMVF NBZ NBUDI B QB॒FSO WBSJBCMF BOOPUBUFE XJUI B OFHBUJWF JOUFSTFDUJPO PS VOJPO UZQF FJUIFSWJB UIF OFHBUJWF WBSJBCMF DBTF PS WJB UIF JOUFSTFDUJPOVOJPO DBTF य़F GPMMPXJOH MFNNB NBLFT DMFBSUIBU XF HFU UIF TBNF TVCTUJUVUJPO BT PVUQVU FJUIFS XBZ-५ॳॳ१  *G v/(x : A) ⇒ 𝜎 UIFO 𝜎 = [x ↦→ v]
1ॸॵॵ६ 3PVUJOF JOEVDUJPO PO A!

य़VT UIJT JTTVF JT OPU B TPVSDF PG OPOEFUFSNJOJTN )PXFWFS UIF USFBUNFOU PG PSQB॒FSOT EPFT
JOUSPEVDF OPOEFUFSNJOJTN " WBMVF v UIBU NBUDIFT UIF QB॒FSOT p1 BOE p2 JO UXP EJ੖FSFOU XBZTDBO BMTP NBUDI p1 |p2 JO CPUI XBZT य़F UZQF TZTUFN XJMM SVMF PVU TVDI OPOEFUFSNJOJTUJD FYBNQMFTCZ FOTVSJOH POMZ POF TJEF PG BO PSQB॒FSO FWFS NBUDIFT *O PUIFS XPSET XFMMUZQFE PSQB॒FSOT
BSF FYDMVTJWF BOE QB॒FSO NBUDIJOH JT EFUFSNJOJTUJD PWFS XFMMUZQFE QB॒FSOT%VBMMZ F/𝑝ˆ ⇒ 𝜎 ↩→ B NFBOT UIBU UIF FMJNJOBUJPO GSBNF F NBUDIFT UIF QB॒FSO 𝑝ˆ XIFSF UIFTVCTUJUVUJPO 𝜎 DPOUBJOT CJOEJOHT GPS QB॒FSO WBSJBCMFT BOE NBZ BEEJUJPOBMMZ DPOUBJO BO FMJNJOBUJPOˆ य़F UZQF B JT UIFGSBNF य़F OFHBUJPO PG UIJT EF੗OJUJPO F/𝑝ˆ " NFBOT UIBU F EPFT OPU NBUDI 𝑝FYQFDUFE SFUVSO UZQF PG UIF DBTF PG UIF 𝜆FYQSFTTJPO JO XIJDI 𝑝ˆ BQQFBSTय़F ∗ FMJNJOBUJPO QB॒FSOT CFIBWF JO B EVBM XBZ UP WBSJBCMF QB॒FSOT 5P VOEFSTUBOE UIFN JU JT
IFMQGVM UP TFF BO FYBNQMF $POTJEFS UIF UFSN e = 𝜆{(∗ ↩→ (A → B)) ↦→ v} v ( )FSF F = [·]v ( BOE𝑝ˆ = ∗ ↩→ A → B य़F NBUDIJOH QSPDFEVSF QSPDFFET CZ SFDVSTJWFMZ NBUDIJOH F BHBJOTU UIF QB॒FSO(x : A) ↩→ B *O UIF FOE UIF SFTVMU JT [ ∗ ↦→ [·]v (] XJUI B SFUVSO UZQF PG B य़VT e ↦−→ (v v ( : B)
"T XJUI WBSJBCMF QB॒FSOT GPS QPTJUJWF UZQFT ∗ QB॒FSOT GPS GVODUJPO BOE QPMZNPSQIJD UZQFT BSF
EF੗OFE JO UFSNT PG NPSF QSJNJUJWF QB॒FSOT 5P LFFQ F⊲⊳ ‫۝‬T UZQFDIFDLJOH EFUFSNJOJTUJD IPXFWFS UIFMBOHVBHF JODMVEFT OFJUIFS BOEFMJNJOBUJPO QB॒FSOT OPS PSFMJNJOBUJPO QB॒FSOT य़VT ∗ QB॒FSOT
GPS VOJPO BOE JOUFSTFDUJPO UZQFT NVTU CF USFBUFE TQFDJBMMZ य़JT JO F੖FDU Pਗ਼PBET UIF OPOEFUFSNJOJTN UP UIF TVCUZQJOH BMHPSJUIN य़F EVBM SPMF PG FMJNJOBUJPO QB॒FSOT XIFO DPNQBSFE XJUI WBMVFQB॒FSOT DBO CF DPVOUFSJOUVJUJWF XIFO JU DPNFT UP VOJPO BOE JOUFSTFDUJPO UZQFT 'PS FYBNQMF B
WBMVF NBUDIFT B WBMVF QB॒FSO x : A1 % A2 XIFO JU NBUDIFT POF PG FJUIFS x : A1 PS x : A2 CVU BOFMJNJOBUJPO GSBNF NBUDIFT BO FMJNJOBUJPO QB॒FSO ∗ ↩→ A1 % A2 XIFO JU NBUDIFT CPUI ∗ ↩→ A1
BOE ∗ ↩→ A2  4JNJMBSMZ 𝜎1 # 𝜎2 JT VTFE UP DPNCJOF TVCTUJUVUJPOT EVSJOH FMJNJOBUJPO NBUDIJOH GPSVOJPO UZQFT XIJMF UIF EVBM 𝜎1 % 𝜎2 PQFSBUJPO JT VTFE GPS JOUFSTFDUJPO UZQFT 5:1& 4:45&.
8F OPX QSFTFOU UIF UZQF TZTUFN PG F⊲⊳  *U BJNT UP HVBSBOUFF CPUI B DPOWFOUJPOBM UZQF TPVOEOFTTQSPQFSUZ BT XFMM BT EFUFSNJOJTN PG SFEVDUJPO

4VCUZQJOH

5ZQFT GPSN B CPVOEFE EJTUSJCVUJWF MB॒JDF VOEFS UIF TVCUZQJOH SFMBUJPO XSJ॒FO A ≤ B EF੗OFE JO'JHVSF  य़F TUBOEBSE TVCUZQJOH SVMFT GPS GVODUJPO VOJPO BOE JOUFSTFDUJPO UZQFT BSF JODMVEFE JOUIJT EF੗OJUJPO PS EFSJWBCMF GSPN UIF SVMFT UIBU BSF 'PS FYBNQMF UIF SVMF
B≤A

A( ≤ B(

A → A( ≤ B → B(

1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

" #PXUJF GPS B #FBTUEFDMBSBUJWF TVCUZQJOH

A≤B
A1 ≤ A2A≤A

A2 ≤ A3A≤B

A1 ≤ A3A2 ≤ A1cA≤cB

A1 ≤ BA1 → B ≤ A2 → B

A≤B

C→A≤C→B
A2 ≤ BA1 # A2 ≤ B

A ≤ B2A ≤ B1 # B2(c A) # (c B) ≤ c (A # B)

∀ 𝛼 .(A % B) ≤ (∀ 𝛼 .A) % (∀ 𝛼 .B)
A ≤ B1(A1 → B) # (A2 → B) ≤ (A1 % A2 ) → B∀ 𝛼 .A ≤ ∀ 𝛼 .B

A ≤ B1A1 # A2 ≤ B(C → A) # (C → B) ≤ (C → A # B)(∀ 𝛼 .A) # (∀ 𝛼 .B) ≤ (∀ 𝛼 .A # B)

A≤B

c (A % B) ≤ (c A) % (c B)

A ≤ B2A ≤ B1 % B2

A ≤ B1 % B2⊥≤BA1 ≤ BA2 ≤ B

NFSHFBCJMJUZ

A ⊲⊳ax B(A % B) # C ≤ (A # C) % (B # C)A≤,

A1 % A2 ≤ B'JH  %FDMBSBUJWF 4VCUZQJOH
A ⊲⊳ BA ⊳⊲ B(

A → A ⊲⊳ B → B
A ⊲⊳ BB ⊲⊳ B((A → B ⊲⊳ A → B

A ⊲⊳ B(A ( ⊲⊳ B

A ⊲⊳ B(∀ 𝛼 .A ⊲⊳ ∀ 𝛼 .B(

A % A ⊲⊳ B

A ⊲⊳ BA # A ⊲⊳ B
A ⊲⊳ax B

B ⊲⊳ AA ⊲⊳ BA ⊲⊳ BEJTUJOHVJTIBCJMJUZA ⊳⊲ Bc A ⊳⊲ c B

A ( ⊳⊲ B

A ⊳⊲ B(

A % A ⊳⊲ B
A ⊳⊲ B (, ⊲⊳ax B(

A ⊳⊲ B

NFSH BYJPNT

A ⊳⊲ax B

B ⊳⊲ AA ⊳⊲ BA ⊳⊲ B

A → A ( ⊲⊳ax ∀ 𝛼 .B
A ⊳⊲ax B

EJTU BYJPNT⊥ ⊳⊲ax B
c1 ≠ c2

B ≤ B(

c1 A ⊳⊲ax c2 B

A ⊳⊲ B'JH  %JTKPJOUOFTT 3FMBUJPOTJT EFSJWBCMF GSPN USBOTJUJWJUZ BOE UIF DP BOE DPOUSBWBSJBODF SVMFT GPS UIF GVODUJPO UZQF DPOTUSVDUPS4VCUZQJOH JT EF੗OFE UP CF SF੘FYJWF BOE USBOTJUJWF "EEJUJPOBMMZ VOJPOT BOE JOUFSTFDUJPOT EJTUSJCVUFPWFS NPTU PUIFS UZQFT य़F GPMMPXJOH UZQF FRVJWBMFODFT IPME
c (A % B)(C → A) # (C → B)≡≡(c A) % (c B)
C → (A # B)

∀ 𝛼 .(A # B)
(A → C) # (B → C)≡≡(∀ 𝛼 .A) # (∀ 𝛼 .B)(A % B) → C

य़F OPUBUJPO A ≡ B EFOPUFT TVCUZQJOH JO CPUI EJSFDUJPOT%VF UP UIF QSFTFODF PG PWFSMPBEJOH XF EP OPU JO HFOFSBM IBWF (A → A()#(B → B () ≤ (A%B) →(A( # B () $POTJEFS BO PWFSMPBEFE GVODUJPO XIJDI QSPEVDFT BO JOUFHFS XIFO HJWFO BO JOUFHFS BOEQSPEVDFT B CPPMFBO XIFO HJWFO B CPPMFBO *U IBT UZQF (Int → Int) # (Bool → Bool) *U DBOOPU CF
DBTU UP UIF UZQF (Int % Bool) → (Int # Bool) CFDBVTF HJWFO POMZ POF PG BO JOUFHFS PS CPPMFBO JU
JT BCMF UP QSPEVDF B WBMVF PG POMZ POF PG UIPTF UZQFT BT B SFTVMUۘOPU CPUI
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

/JDL 3JPVY 9VFKJOH )VBOH #SVOP $ E 4 0MJWFJSB BOE 4UFWF ;EBODFXJDUZQF XFMMGPSNFEOFTT

Γ/A
𝛼∈Γ
Γ/𝛼

Γ/A

Γ/A

Γ/cA
Γ / A1

Γ/B

Γ/A→B

Γ / A2A1 ⊲⊳ A2

Γ / A1 # A2

Γ, 𝛼 / BΓ / ∀ 𝛼 .B
Γ / A1Γ/,Γ / A2Γ/⊥

A1 ⊳⊲ A2

Γ / A1 % A2

'JH  8FMM'PSNFE 5ZQFT%JTKPJOU BOE 8FMM'PSNFE 5ZQFT

य़F NFSHFBCJMJUZ BOE EJTUJOHVJTIBCJMJUZ SFMBUJPOT BSF EF੗OFE JOEVDUJWFMZ JO 'JHVSF .FSHFBCJMJUZ य़F JEFB PG NFSHFBCJMJUZ JT UP SFMBUF UXP UZQFT A BOE B XIFO UIFSF JT OP QPUFOUJBMMZ
BNCJHVPVT PQFSBUJPO TIBSFE CFUXFFO UIFN $POTJEFS UIF GPMMPXJOH EFSJWBCMF SVMFTl≠k

A ⊲⊳ B{l : A} ⊲⊳ {k : B}{l : A} ⊲⊳ {l : B}

य़F ੗STU TUBUFT UIBU BOZ SFDPSET XJUI EJ੖FSFOU MBCFMT BSF NFSHFBCMF CFDBVTF TVDI UZQFT TIBSF OP
PQFSBUJPOT JO DPNNPO य़F TFDPOE TUBUFT UIBU FWFO XIFO UXP UZQFT CPUI DPOUBJO UIF ੗FME l UIFZNBZ CF NFSHFE JG UIF DPOUFOUT PG UIF ੗FME UIFNTFMWFT BSF NFSHFBCMF *O UIJT DBTF TPNF MBUFS QBSUPG FWFSZ PQFSBUJPO PO UIF UXP UZQFT BॏFS UIF QSPKFDUJPO PG l XJMM EJTBNCJHVBUF B VTF PG UIJT UZQF
य़FTF UXP SVMFT GPMMPX EJSFDUMZ GSPN UIF ੗STU UXP SVMFT PG 'JHVSF  'VODUJPOT DBO CF NFSHFEXIFO UIFJS BSHVNFOUT BSF EJTUJOHVJTIBCMF UP GPSN BO PWFSMPBEFE GVODUJPO 5XP GVODUJPOT UIBU
UBLF UIF TBNF BSHVNFOU UZQF DBO BMTP CF NFSHFE XIFO UIFJS PVUQVUT DBO CF 8F QSFWJPVTMZ TBXBO FYBNQMF JO XIJDI NFSHJOH B DPOTUSVDUPS PG UZQF Int → {age : Int} XJUI BOPUIFS PG UZQF
Int → {name : String} ZJFMET B DPNCJOFE DPOTUSVDUPS PG UZQF Int → {age : Int, name : String}य़JT TUZMF PG NFSHF TVQQPSUT OFTUFE DPNQPTJUJPO BOE JT BMTP QPTTJCMF GPS VOJWFSTBMMZ RVBOUJ੗FEUZQFT " NFSHF PG WBMVFT PG UZQFT A BOE A( JUTFMG IBWJOH UZQF A # A( DBO CF NFSHFE XJUI BUIJSE WBMVF PG UZQF B XIFO CPUI A BOE A( BSF NFSHFBCMF XJUI B य़JT FOTVSFT UIBU PQFSBUJPOT PO
B EP OPU DPO੘JDU XJUI UIPTF PG A PS A( 4JODF B WBMVF PG UZQF A % A( NBZ BDUVBMMZ IBWF FJUIFSUZQF A PS A( GPS UIJT VOJPO UZQF UP CF NFSHFBCMF XJUI BOPUIFS UZQF CPUI A BOE A( NVTU CF "WBMVF PG UZQF , DBOOPU CF VTFE JO BOZ XBZ य़VT UIJT UZQF DBO USJWJBMMZ CF NFSHFE XJUI BOZ PUIFSUZQF 'JOBMMZ CFDBVTF BQQMJDBUJPO PG UFSNT UP UZQFT JT FYQMJDJU JO F⊲⊳ JU JT TBGF GPS GVODUJPO UZQFTBOE VOJWFSTBM RVBOUJ੗FST UP CF NFSHFBCMF XJUI FBDI PUIFS *O TZTUFNT XIFSF VOJWFSTBM RVBOUJ੗FSTIBWF OP FYQMJDJU FMJNJOBUJPO GPSN UIJT NBZ OPU CF QPTTJCMF
%JTUJOHVJTIBCJMJUZ 'JHVSF  BMTP HJWFT UIF EJTUJOHVJTIBCJMJUZ SFMBUJPO 5XP UZQFT A BOE B BSF EJTUJOHVJTIBCMF XIFO QB॒FSOT PG FBDI UZQF EP OPU NBUDI WBMVFT PG UIF PUIFS UZQF *O PUIFS XPSETEJTUJOHVJTIBCJMJUZ NFBOT UIBU UIF QB॒FSO NBUDIJOH QSPDFEVSF DBO UFMM WBMVFT PG POF UZQF GSPN WBMVFT PG UIF PUIFS .PTU PG UIF EJTUJOHVJTIBCJMJUZ SVMFT BSF TUSBJHIUGPSXBSE PS QSFDJTFMZ EVBM UP UIPTF
PG NFSHFBCJMJUZ " LFZ SVMF TUBUFT UIBU VOFRVBM UZQF DPOTUSVDUPST BSF EJTUJOHVJTIBCMF "OPUIFS SVMF
DMPTFT EJTUJOHVJTIBCJMJUZ PWFS UIF TVCUZQJOH SFMBUJPO "T TIPXO JO g UIJT QSPQFSUZ JT JNQPSUBOUGPS TPVOEOFTT PG UIF UZQF TZTUFN
8FMM'PSNFE 5ZQFT य़F XFMMGPSNFEOFTT SFMBUJPO PO UZQFT XSJ॒FO Γ / A FOTVSFT UIBU 0OMZ UIF UZQF WBSJBCMFT JO Γ BQQFBS GSFF JO A य़F DPNQPOFOUT PG FWFSZ JOUFSTFDUJPO JO A BSF NFSHFBCMF
 य़F DPNQPOFOUT PG FWFSZ VOJPO JO A BSF EJTUJOHVJTIBCMF

1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

" #PXUJF GPS B #FBTUय़F DBTFT GPS VOJPOT BOE JOUFSTFDUJPO UZQFT BSF UIF POMZ OPOTUBOEBSE QBSU PG UIF EF੗OJUJPO PG UIJTSFMBUJPO XIJDI JT HJWFO JO 'JHVSF य़F EJTKPJOUOFTT SFTUSJDUJPOT DPOTJEFSBCMZ TJNQMJGZ UIF UZQF TPVOEOFTT BSHVNFOU CZ FOBCMJOHJOWFSTJPO QSJODJQMFT UIBU XF XJMM TFF JO g *O UIF DBTF PG VOJPOT UIF SFTUSJDUJPOT TJNJMBSMZ TJNQMJGZUIF QB॒FSO NBUDIJOH QSPDFEVSF $POTJEFS NBUDIJOH UIF WBMVF v = 𝜆{(∗ ↩→ A % B) ↦→ v ( } BHBJOTUUIF QB॒FSO p = (x : A)| (x : B) य़F NBUDIJOH QSPDFEVSF XF TBX FBSMJFS XPVME USZ UP NBUDI v
BHBJOTU x : A BOE x : B TFQBSBUFMZ #VU UIFTF NBUDIFT BSF QPUFOUJBMMZ JMM UZQFE A % B JT JO HFOFSBM B
TVCUZQF PG OFJUIFS A OPS B 8JUI UIF EJTKPJOUOFTT SFTUSJDUJPO PO VOJPOT JU DBO CF QSPWFO UIBU FWFSZ
WBMVF PG UZQF A % B FJUIFS IBT UZQF A PS UZQF B य़VT POF PG UIF UXP NBUDIFT JT XFMM UZQFE" OPUBCMF ESBXCBDL PG UIF EJTKPJOUOFTT SFTUSJDUJPO JT UIBU JU QSFDMVEFT FNQMPZJOH JOUFSTFDUJPOTBT UZQF SF੗OFNFOUT <'SFFNBO BOE 1GFOOJOH > *U BQQFBST UIBU VOEFS B OPUJPO PG TVCUZQJOHXJUI UIF SJHIU EJTUSJCVUJWJUZ SVMFT OPOEJTUJOHVJTIBCMF VOJPOT BOE UIFJS QB॒FSOT DBO PॏFO CF
TJNQMJ੗FE UP EJTUJOHVJTIBCMF POFT 'VUVSF XPSL NBZ TUVEZ TVDI BO BQQSPBDI UP TVQQPSU BSCJUSBSZVOJPO BOE JOUFSTFDUJPO UZQFT JO F⊲⊳  'PS PVS QSFTFOU QVSQPTFT EJTKPJOU JOUFSTFDUJPOT BOE VOJPOTDBQUVSF UIF FTTFODF PG XIBU JT OFDFTTBSZ UP JOWFTUJHBUF PWFSMPBEJOH BOE FYUFOTJCMF EBUB UZQFT5ZQJOH'JHVSF  EF੗OFT F⊲⊳ ‫۝‬T UZQF TZTUFN *U CPSSPXT TPNF DPODFQUT GSPN CJEJSFDUJPOBM UZQJOH XIJDI IFMQFOTVSF UIBU UIF SVMFT BSF UZQFEJSFDUFE य़F KVEHNFOU Γ / e ⇒ A ۠e TZOUIFTJ[FT UZQF A VOEFS ΓۡNFBOT UIBU A JT UIF MFBTU UZQF XIJDI DBO CF BTTJHOFE UP e *O PUIFS XPSET A JT UIF QSJODJQBM UZQF
PG e .FBOXIJMF Γ / e ⇐ A ۠e DIFDLT BU UZQF A VOEFS Γۡ TJHOJ੗FT UIBU e IBT UIF UZQF A BOE
QPUFOUJBMMZ TPNF TVCUZQFT PG A *U JT EF੗OFE CZ B TJOHMF SVMF BOE IPMET QSFDJTFMZ XIFO e TZOUIFTJ[FTTPNF TVCUZQF PG A VOEFS Γ 6OMJLF UZQJDBM CJEJSFDUJPOBM TZTUFNT UIF EJTUJODUJPO CFUXFFO DIFDLJOHBOE TZOUIFTJT JT OPU FYQMPJUFE UP SFEVDF UIF OFFE GPS UZQF BOOPUBUJPOTˆ ⇒ C य़JT JT"QQMJDBUJPOT BSF UZQFE XJUI UIF IFMQ PG B UZQFMFWFM EJTQBUDI PQFSBUPS disp(A, 𝐵)
TJNJMBS JO TUZMF UP UIF 𝑎𝑝𝑝𝑡𝑦𝑝𝑒 GVODUJPO JO UIF TZTUFN PG 'SFFNBO BOE 1GFOOJOH <> य़F disp
NFUBGVODUJPO UBLFT UIF UZQF PG B GVODUJPO A BOE B DPOUFYU 𝐵ˆ BOE DPNQVUFT UIF PVUQVU UZQF C%VF UP PWFSMPBEJOH BOE VOJPO UZQFT UIF JNQMFNFOUBUJPO PG UIJT PQFSBUJPO JT OPOUSJWJBM *U NVTUTUBUJDBMMZ EFUFSNJOF XIJDI PWFSMPBET PG B GVODUJPO XJMM FYFDVUF 8F XJMM DPWFS UIJT JO g *U JT
IPXFWFS FYQFDUFE UP BCJEF CZ UIF GPMMPXJOH TQFD
-५ॳॳ१  4ॵॻॴ४ॴ५ॹॹ १ॴ४ $ॵॳॶॲ५ॺ५ॴ५ॹॹ ॵ६ 5ॿॶ५ংॲ५ॼ५ॲ %९ॹॶ१ॺ३८ 
 8F IBWF disp(A, B) ⇒ C Jञ C JT UIF MFBTU UZQF TVDI UIBU A ≤ B → C 8F IBWF disp(A, [B]) ⇒ C Jञ C JT UIF MFBTU UZQF TVDI UIBU UIFSF FYJTUT A( XIFSF A ≤ ∀ 𝛼 .A(
BOE C ≤ A( [B/𝛼]

.FSHFT BSF UZQFE CZ UBLJOH UIF JOUFSTFDUJPO PG UIF UZQFT UIFZ BSF BOOPUBUFE XJUI य़FTF UZQFT
NVTU CF NFSHFBCMF 5ZQFT BSF BTTJHOFE UP B 𝜆WBMVF CZ PCUBJOJOH B UZQF GPS FBDI DMBVTF JO JUT CPEZFOTVSJOH UIBU UIF JOGFSSFE UZQFT PG BMM DMBVTFT BSF EJTKPJOU BOE DPOTUSVDUJOH BO JOUFSTFDUJPO PG UIPTF
UZQFT य़JT JOWPMWFT BO BVYJMJBSZ KVEHNFOU Γ; 𝑝ˆ / e ⇒ A XIJDI JOGFST UIF UZQF A PG B TJOHMF DMBVTF
𝑝ˆ ↦→ e *OGFSSJOH UIF UZQF PG B DMBVTF JOWPMWFT EFUFSNJOJOH UIF UZQFT PG UIF CPVOE WBSJBCMFT JO 𝑝ˆ
BT XFMM BT UIJT QB॒FSO‫۝‬T SFUVSO UZQF BOOPUBUJPO य़FTF BSF VTFE UP UZQF UIF FYQSFTTJPO eय़F OFYU UXP KVEHNFOUT UZQF QB॒FSOT 7BMVF QB॒FSOT BSF UZQFE XJUI UIF KVEHNFOU Γ / p ⇒A 1 Δ य़F FOWJSPONFOU Γ DPOUBJOT UIF UZQF WBSJBCMFT GSFF JO p BT XFMM BT A B BOE Δ  य़F UZQF A
JT UIF UZQF PG WBMVF UIBU p NBUDIFT JF UIF UZQF UIBU p FMJNJOBUFT  -BTUMZ Δ DPOUBJOT UIF UZQF BOE
UFSN WBSJBCMFT CPVOE CZ p
"O PSQB॒FSO CJOET POMZ UIF WBSJBCMFT UIBU BSPVOE CPVOE CZ CPUI TVCQB॒FSOT य़JT FOTVSFT UIBUBU SVOUJNF UIFSF JT BMXBZT B WBMVF UP BTTJHO UP FWFSZ CPVOE WBSJBCMF FWFO JG POMZ POF TVCQB॒FSONBUDIFT 0O UIF PUIFS IBOE BO BOEQB॒FSO CJOET UIF WBSJBCMFT UIBU BSF NFOUJPOFE PO FJUIFS TJEF
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

/JDL 3JPVY 9VFKJOH )VBOH #SVOP $ E 4 0MJWFJSB BOE 4UFWF ;EBODFXJDFYQSFTTJPO UZQF TZOUIFTJTDIFDLJOH

Γ/e⇔A
x:A∈Γ

Γ/e ⇒ AΓ/x ⇒ AΓ/e ⇐ AΓ/e ⇒ AΓ / (e : A) ⇒ A

Γ/ce ⇒ cA

Γ / e2 ⇒ A2
Γ / e1 ⇒ A1
disp(A1, A2 ) ⇒ B

Γ/e ⇐ B

Γ / A2disp(A1, [A2 ]) ⇒ B

Γ / e ⇒ A1

Γ / e1 e2 ⇒ B

Γ / e [A2 ] ⇒ B−
Γ / 𝐴−
Γ / 𝐴−
𝐴−
1
2
1 ⊲⊳ 𝐴2
Γ / e1 ⇐ 𝐴 −Γ / e2 ⇐ 𝐴−1
2

Γ; 𝑝ˆ1 / e1 ⇒ A1, ... , Γ; 𝑝ˆn / en ⇒ An
A1 ⊲⊳ ... ⊲⊳ An−−−
Γ / (e1 : 𝐴−1 ) ! (e2 : 𝐴2 ) ⇒ 𝐴1 # 𝐴2

Γ / 𝜆{𝑝ˆ1 ↦→ e1, ... , 𝑝ˆn ↦→ en } ⇒ A1 # ... # An
WBMVF QBࡇFSO UZQJOH

Γ/𝑝 ⇒A1Δ
Γ/AΓ / p1 ⇒ A1 1 Δ1

Γ / (x : A) ⇒ A 1 x : A
Γ/p⇒A1Δ

Γ/cp⇒cA1Δ
Γ; 𝑝ˆ / e ⇒ BA≤B

𝜆 DMBVTF UZQJOH

Γ / 𝑝ˆ ⇒ A ↩→ B 1 Δ
Γ, Δ / e ⇐ BΓ; 𝑝ˆ / e ⇒ A

Γ / p2 ⇒ A2 1 Δ2

A1 ⊳⊲ A2

Γ / p1 |p2 ⇒ A1 % A2 1 Δ1 % Δ2

Γ / p1 ⇒ A1 1 Δ1

Γ / p2 ⇒ A2 1 Δ2

A1 ⊲⊳ A2

Γ / p1 &p2 ⇒ A1 # A2 1 Δ1 # Δ2

Γ / 𝑝ˆ ⇒ A ↩→ B 1 Δ
Γ / 𝐵−−

p1 ∼ p2

FMJNJOBUJPO QBࡇFSO UZQJOH

−

Γ/B

−

Γ / (∗ ↩→ 𝐵 ) ⇒ 𝐵 ↩→ 𝐵 1 ·Γ/p⇒A1Δ

Γ / (p ↩→ B) ⇒ (A → B) ↩→ B 1 Δ
Γ, 𝛼 / BΓ / (𝛼 ↩→ B) ⇒ ∀ 𝛼 .B ↩→ B 1 𝛼
WBMVF QBࡇFSO DPOTJTUFODZ

𝑝1 ∼ 𝑝2(x : A) ∼ (y : B)

𝑝1 ∼ 𝑝2

𝑝1 ∼ 𝑝2

𝑝 1 &𝑝 1( ∼ 𝑝 2

c 𝑝1 ∼ c 𝑝2

Δ1 % Δ2 BOE Δ1 # Δ2

𝑝 1( ∼ 𝑝 2

𝑝1 ∼ 𝑝2

𝑝 1 ∼ 𝑝 2(

𝑝 1 ∼ 𝑝 2 &𝑝 2(

x : A ∈ (Δ1 % Δ2 )J੖x : A1 ∈ Δ1 BOE x : A2 ∈ Δ2 BOE A = A1 % A2

x : A1 ∈ (Δ1 # Δ2 )x : A2 ∈ (Δ1 # Δ2 )x : A1 # A2 ∈ (Δ1 # Δ2 )

JG
JG
JG

x : A1 ∈ Δ1 BOE x ∉ dom (Δ2 )x : A2 ∈ Δ2 BOE x ∉ dom (Δ1 )x : A1 ∈ Δ1 BOE x : A2 ∈ Δ2

'JH  5ZQJOH 3VMFT

य़F Δ1 % Δ2 BOE Δ1 # Δ2 PQFSBUJPO UBLF DBSF PG CVJMEJOH UIF PVUQVU FOWJSPONFOUT JO UIF UZQJOH PG
UIFTF LJOET PG QB॒FSOT य़FJS EF੗OJUJPOT BSF SFNJOJTDFOU PG DMBTTJDBM SFDPSE TVCUZQJOH
0OF TVCUMF QPJOU JO UIF EF੗OJUJPO PG WBMVF QB॒FSO NBUDIJOH JT SFRVJSFE UP FOTVSF EFUFSNJOJTN
8F OFFE UP SVMF PVU DFSUBJO QB॒FSOT MJLF (x : ,)&c0 (x : (c1 , % c2 ,)) UIBU CJOE UIF TBNF WBSJBCMF
UXJDF UP EJTUJODU WBMVFT य़JT JT BDIJFWFE CZ SFRVJSJOH UIBU UIF UXP TJEFT PG BO BOEQB॒FSO BSF
DPOTJTUFOU XSJ॒FO p1 ∼ p2  &MJNJOBUJPO QB॒FSOT BSF UZQFE XJUI UIF KVEHNFOU Γ / 𝑝ˆ ⇒ A ↩→ B 1 Δ
य़F FOWJSPONFOUT Γ BOE Δ QFSGPSN UIF TBNF GVODUJPOT BT GPS WBMVF QB॒FSOT य़F UZQF A UIJT UJNF
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

" #PXUJF GPS B #FBTUJT UIF UZQF PG DPOUFYU UIBU 𝑝ˆ NBUDIFT JF UIF UZQF UIBU 𝑝ˆ JOUSPEVDFT  4JODF FMJNJOBUJPO QB॒FSOTˆDPOUBJO PVUQVU UZQF BOOPUBUJPOT B JT UZQF PG UIF FYQSFTTJPO CPVOE VOEFS 𝑝&YBNQMF $POTJEFS UIF WBMVF 𝜆{(c (f : Bool → Bool) ↩→ Int) ↦→ if f true then 1 else 0} PG UZQF
(c (Bool → Bool)) → Int य़JT GVODUJPO QB॒FSO NBUDIFT PO JUT JOQVU UP FYUSBDU B GVODUJPO f GSPN
VOEFSOFBUI B DPOTUSVDUPS c य़FO JU DBMMT UIF GVODUJPO BOE SFUVSOT BO JOUFHFS CBTFE PO UIF SFTVMUय़F FMJNJOBUJPO QB॒FSO 𝑝ˆ = c (f : Bool → Bool) ↩→ Int JT UZQFE XJUI UIF GPMMPXJOH EFSJWBUJPO
· / (f : Bool → Bool) ⇒ Bool → Bool 1 f : Bool → Bool

· / c (f : Bool → Bool) ⇒ c (Bool → Bool) 1 f : Bool → Bool
· / 𝑝ˆ ⇒ (c (Bool → Bool) → Int) ↩→ Int 1 f : Bool → Bool"U UIF CP॒PN JO UIF FMJNJOBUJPO QB॒FSO KVEHNFOU OPUF UIBU UIF UZQF Int BQQFBST UXJDF य़F ੗STUPDDVSSFODF JT UP UIF SJHIU PG UIF → JO UIF UZQF XIJDI CFDPNFT UIF UZQF PG UIF FOUJSF GVODUJPO य़F
TFDPOE JT UP UIF SJHIU PG UIF ↩→ BT UIF SFUVSO UZQFۘUIBU JT UIF UZQF PG UIF CPEZ if f true then 1 else 0

5:1*/( "-(03*5).

य़F EJTUJOHVJTIBCJMJUZ TVCUZQJOH BOE UZQFMFWFM EJTQBUDI SFMBUJPOT IBWF UIVT GBS CFFO QSFTFOUFE
POMZ JO B EFDMBSBUJWF NBOOFS 8F IFSF EJTDVTT UIF BMHPSJUINT SFRVJSFE UP DPNQVUF UIFTF SFMBUJPOT"T CPUI PG UIFTF QMBZ DSVDJBM SPMFT JO UIF UZQF TZTUFN UIFJS JNQMFNFOUBUJPOT BSF OFDFTTBSZ UP TIPXUIF UZQJOH SFMBUJPO JT DPNQVUBCMF


4QMJࣄJOH 4VCUZQJOH BOE %JTKPJOUOFTTय़F NBJO EJਖ਼DVMUZ JO PVS TVCUZQJOH BMHPSJUIN EFTJHO BSJTFT GSPN UIF EJTUSJCVUJWJUZ PWFS JOUFSTFDUJPOT BOE VOJPOT " DPOWFOUJPOBM UFDIOJRVF BEBQUFE CZ NBOZ PG UIF TZTUFNT UIBU TVQQPSU CPUIJOUFSTFDUJPO BOE VOJPO UZQFT JT UP DPOWFSU UZQFT UP TUBOEBSE GPSNT CFGPSF BOBMZ[JOH UIFN <$BTUBHOB 'SFFNBO BOE 1GFOOJOH > 8F JOTUFBE GPMMPX UIF JEFB PG TQMJࡇJOH UZQFT <)VBOH BOE
0MJWFJSB > XIJDI OPSNBMJ[FT UZQFT PO UIF ੘Z BOE FYUFOE JUT TVCUZQJOH UP VOJWFSTBMMZ RVBOUJ੗FE BOE SFDPSE UZQFT य़F UXP TQMJ॒JOH BMHPSJUINT TIPXO BU UIF UPQ PG 'JHVSF  FBDI UBLF B UZQF
BOE USBOTGPSN JU JOUP BO FRVJWBMFOU VOJPO PS JOUFSTFDUJPO UZQF SFTQFDUJWFMZ य़F UZQF C → A # B
GPS JOTUBODF JT FRVJWBMFOU UP (C → A) # (C → B) BT XF DBO EFSJWF spliti (C → A # B) ⇒ (C →A) # (C → B) 8F VTF B OFHBUFE BSSPX UP FYQSFTT UIBU B UZQF JT OPU TQMJ॒BCMF FH splitu (Int) "य़FTF SVMFT FODPEF BMM PG UIF EJTUSJCVUJWJUZ JO TVCUZQJOH BOE UIFSFGPSF UBLF UIF CVSEFO P੖ UIF BMHPSJUINJD TVCUZQJOH SVMFT EF੗OFE JO UIF NJEEMF PG 'JHVSF   0ODF XF SFQMBDF UIFTF UZQF TQMJ॒JOH
KVEHNFOUT CZ FRVBUJPOT JF XSJUF A = A1 # A2 BOE B = B1 % B2 JOTUFBE PG spliti (A) ⇒ A1 # A2
BOE splitu (B) ⇒ B1 % B2 UIF EJTUSJCVUJWJUZ JT GVMMZ FMJNJOBUFE BOE XF DBO TFF UIBU UIF BMHPSJUINJD
TVCUZQJOH SVMFT GPMMPX B TUBOEBSE QSFTFOUBUJPO *NQPSUBOUMZ JU DPJODJEFT XJUI EFDMBSBUJWF TVCUZQ
JOH-५ॳॳ१  4ॵॻॴ४ॴ५ॹॹ १ॴ४ $ॵॳॶॲ५ॺ५ॴ५ॹॹ ॵ६ "ॲ७ॵॸ९ॺ८ॳ९३ 4ॻ२ॺॿॶ९ॴ७ A ≤ B JG BOE POMZ JG A ≤alg B

1ॸॵॵ६ 0VS QSPPG GPMMPXT UIBU PG )VBOH BOE 0MJWFJSB <> य़F POMZ JG EJSFDUJPO TPVOEOFTTJT TUSBJHIUGPSXBSE JU GPMMPXT GSPN UIF TPVOEOFTT PG UIF UZQF TQMJ॒JOH SFMBUJPOTय़F LFZ UP QSPWJOH UIF JG EJSFDUJPO DPNQMFUFOFTT JT EFNPOTUSBUJOH UIF USBOTJUJWJUZ PG UIF BMHPSJUINJD TZTUFN 'PS UIJT XF JOEVDU PO UIF TVN PG UIF TJ[FT PG UIF UXP UZQFT 8IFO B UZQF JT
TQMJU XF IBWF BO JOEVDUJPO IZQPUIFTJT GPS FBDI QJFDF 'SPN UIFSF UIF QSPPG NBLFT VTF PG BVYJMJBSZJOWFSTJPO QSPQFSUJFT
!
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

/JDL 3JPVY 9VFKJOH )VBOH #SVOP $ E 4 0MJWFJSB BOE 4UFWF ;EBODFXJDˆ ⇒ A1 % A2
splitu (𝐴)VOJPO TQMJࡇJOH
splitu (A) ⇒ A1 % A2

splitu (A % B) ⇒ A % B

splitu (A) ⇒ A1 % A2

splitu (∀ 𝛼 .A) ⇒ (∀ 𝛼 .A1 ) % (∀ 𝛼 .A2 )splitu (A) ⇒ A1 % A2

splitu (c A) ⇒ c A1 % c A2

splitu (A) "splitu (A # B) ⇒ (A1 # B) % (A2 # B)

splitu (B) ⇒ B1 % B2

splitu (A # B) ⇒ (A # B1 ) % (A # B2 )JOUFSTFDUJPO TQMJࡇJOH

spliti (A) ⇒ A1 # A2
spliti (A) ⇒ A1 # A2

spliti (A # B) ⇒ A # B

spliti (A) ⇒ A1 # A2

spliti (∀ 𝛼 .A) ⇒ (∀ 𝛼 .A1 ) # (∀ 𝛼 .A2 )spliti (B) ⇒ B1 # B2

spliti (A → B) ⇒ (A → B1 ) # (A → B2 )spliti (c A) ⇒ c A1 # c A2

spliti (B) "splitu (A) ⇒ A1 % A2

spliti (A) "spliti (B) ⇒ B1 # B2

spliti (A → B) ⇒ (A1 → B) # (A2 → B)

spliti (A) ⇒ A1 # A2

spliti (A % B) ⇒ (A1 % B) # (A2 % B)

spliti (A % B) ⇒ (A % B1 ) # (A % B2 )BMHPSJUINJD TVCUZQJOH

A ≤alg B
A ≤alg B

A ≤alg A

B1 ≤alg A1

c A ≤alg c B

spliti (A) ⇒ A1 # A2
A1 ≤alg B
A ≤alg B

A2 ≤alg B2

A1 → A2 ≤alg B1 → B2

spliti (A) ⇒ A1 # A2
A2 ≤alg B
A ≤alg B

splitu (B) ⇒ B1 % B2

A ≤alg B

A ≤alg B1

A ≤alg B∀ 𝛼 .A ≤alg ∀ 𝛼 .B

⊥ ≤alg A

spliti (B) ⇒ B1 # B2
A ≤alg B1
A ≤alg B2

A ≤alg ,splitu (A) ⇒ A1 % A2
A1 ≤alg B
A2 ≤alg B

A ≤alg B

A ≤alg B

splitu (B) ⇒ B1 % B2

A ≤alg B

A ≤alg B2

ˆ ⇒C
disp(A, 𝐵)

UZQFMFWFM EJTQBUDI

splitu (B) ⇒ B1 % B2
disp(A, B1 ) ⇒ C1
disp(A, B2 ) ⇒ C2
disp(A, B) ⇒ C1 % C2

disp(∀ 𝛼 .A, [B]) ⇒ A[B/𝛼 ]ˆ "splitu ( 𝐵)ˆdisp(⊥, 𝐵) ⇒ ⊥ˆ "splitu ( 𝐵)ˆˆ ⇒ C2disp(A1 , 𝐵) ⇒ C1
disp(A2 , 𝐵)
ˆ ⇒ C1 % C2
disp(A1 % A2 , 𝐵)

ˆ "splitu ( 𝐵)ˆˆ ⇒ C2disp(A1 , 𝐵) "disp(A2 , 𝐵)
ˆ ⇒ C2disp(A1 # A2 , 𝐵)

splitu (B) "(B≤A

disp(A → A , B) ⇒ A(

ˆ "splitu ( 𝐵)ˆˆ "disp(A1 , 𝐵) ⇒ C1
disp(A2 , 𝐵)
ˆ ⇒ C1disp(A1 # A2 , 𝐵)

ˆ "splitu ( 𝐵)ˆˆ ⇒ C2disp(A1 , 𝐵) ⇒ C1
disp(A2 , 𝐵)
ˆ ⇒ C1 # C2
disp(A1 # A2 , 𝐵)

'JH  4VCUZQJOH BOE 3FMBUFE "MHPSJUINT

4JODF UIF EJTUJOHVJTIBCJMJUZ SFMBUJPO JT DMPTFE PWFS TVCUZQJOH EFDJEJOH JU BMTP SFRVJSFT EFBMJOH
XJUI EJTUSJCVUJWJUZ य़VT UIF EJTKPJOUOFTT BMHPSJUIN <3JPVY FU BM C> VTFT TQMJ॒JOH KVTU BT UIFTVCUZQJOH BMHPSJUIN EPFT5ZQJOH "QQMJDBUJPOय़F NFUB GVODUJPO disp(A, B) ⇒ C JT VTFE UP DBMDVMBUF UIF NPTU QSFDJTF PVUQVU UZQF GPS CPUIBQQMJDBUJPOT BOE UZQF BQQMJDBUJPOT य़F GVODUJPO UZQF A IBT B WFSZ HFOFSBM GPSN BT JU EFTDSJCFTPWFSMPBEFE GVODUJPOT PS OFTUFE DPNQPTJUJPOT .FUBWBSJBCMF 𝐵ˆ DBQUVSFT UXP DBTFT JU JT FJUIFS UIF
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

" #PXUJF GPS B #FBTUUFSN‫۝‬T UZQF JO BO PSEJOBSZ BQQMJDBUJPO XIJDI XF VTF B UP SFQSFTFOU PS UIF UZQF BSHVNFOU JO BUZQF BQQMJDBUJPO EFOPUFE CZ [B] य़F EF੗OJUJPOT FOTVSF UIBU UZQF BSHVNFOUT BSF OPU TQMJ॒BCMF *O
PUIFS XPSET splitu ([B]) " IPMET USJWJBMMZय़F CBTF DBTF GPS B UZQF BQQMJDBUJPO JT XIFO B VOJWFSTBM RVBOUJ੗FE UZQF PS B CP॒PN UZQF NFFUTB UZQF BSHVNFOU 6OMJLF JO UIF GVODUJPO BQQMJDBUJPO SVMF XIJDI DIFDLT TVCUZQJOH UIFSF JT OP TJEF
DPOEJUJPO GPS UZQF BQQMJDBUJPO TP XF EP OPU OFFE UP QSPDFTT UIF UZQF BSHVNFOU य़F EJTQBUDIGVODUJPO MPPLT JOUP BMM UIF VOJWFSTBMMZ RVBOUJ੗FE UZQFT JO A TVCTUJUVUFT UIF UZQF BSHVNFOU JOUPUIFJS CPEJFT BOE UIFO SFDPNQPTFT UIFN CBDL JOUP UIF PSJHJOBM TUSVDUVSF BMM UIF CP॒PN UZQFT BSF
BMTP LFQU JO UIF QSPDFTT  'PS FYBNQMF XF IBWF disp((⊥ % ∀ 𝛼 .A), [B]) ⇒ ⊥ % A[B/𝛼]
'PS BO JOUFSTFDUJPO UZQF UP CF BQQMJDBCMF UIF EJTQBUDI GVODUJPO SFRVJSFT UIBU BU MFBTU POF QBSUPG JU JT BQQMJDBCMF *NBHJOF BO PWFSMPBEFE GVODUJPO XJUI UXP JNQMFNFOUBUJPOT UZQFE CZ A1 → A2
BOE B1 → B2 SFTQFDUJWFMZ य़F BSHVNFOU POMZ OFFET UP TBUJTGZ FJUIFS A1 PS B1 GPS BU MFBTU POF
JNQMFNFOUBUJPO UP CF BQQMJDBCMF JO UIF SVOUJNF 'PS VOJPOT JU JT NBOEBUPSZ UIBU CPUI QBSUT BSF
BQQMJDBCMF BT VOJPOT POMZ HVBSBOUFF UIBU POF TJEF JT TBUJT੗FE
%JTQBUDI TQMJUT VOJPOT JO UIF BSHVNFOU UZQF FBHFSMZ 5P TFF XIZ DPOTJEFS UIF GPMMPXJOH TJUVBUJPOXIFSF BO JOUFSTFDUJPO PG UXP GVODUJPO UZQFT JT BQQMJFE UP B VOJPO य़F UXP GVODUJPO UZQFT DBO FBDI
UBLF POF PG UIF QPTTJCMF BSHVNFOU UZQFT CVU XIFO EJSFDUMZ DPNQBSFE XJUI UIF XIPMF BSHVNFOU
UZQF OFJUIFS DBO IBWF UIF TVCUZQJOH DPOEJUJPO TBUJT੗FE
disp(((Int → A1 ) # (Bool → A2 )), Int % Bool) ⇒ A1 % A2

"ॏFS PVS EJTQBUDI GVODUJPO UFBST UIF BSHVNFOU UZQF BQBSU CPUI BQQMJDBUJPOT DBO QSPDFFE"T UIF UZQF PG B UFSN FWPMWFT EVSJOH SFEVDUJPO UIF EJTQBUDI GVODUJPO NVTU CF NPOPUPOJD UPFOTVSF TPVOEOFTT 4QFDJ੗DBMMZ UIF TVCUZQFT PG UXP BQQMJDBCMF UZQFT NVTU BMTP CF BQQMJDBCMF BOEUIF SFUVSO UZQF DPNQVUFE CZ UIF EJTQBUDI GVODUJPO TIPVME CF B TVCUZQF PG UIF PSJHJOBM SFUVSO UZQF
-५ॳॳ१  .ॵॴॵॺॵॴ९३९ॺॿ ॵ६ 5ॿॶ५ং-५ॼ५ॲ %९ॹॶ१ॺ३८ ˆ ⇒ C BOE A( ≤ A UIFO UIFSF FYJTUT C ( ≤ C TVDI UIBU disp(A(, 𝐵)ˆ ⇒ C ( *G disp(A, 𝐵) *G disp(A, B) ⇒ C BOE B ( ≤ B UIFO UIFSF FYJTUT C ( ≤ C TVDI UIBU disp(A, B () ⇒ C (1ॸॵॵ६ 'PMMPXT GSPN UIF UZQFMFWFM EJTQBUDI TQFDJ੗DBUJPO HJWFO CZ -FNNB 
!

3&46-54

8F QSPWF UIF TPVOEOFTT PG F⊲⊳ ‫۝‬T UZQF TZTUFN VTJOH B QSPHSFTT BOE QSFTFSWBUJPO BSHVNFOU <8SJHIU
BOE 'FMMFJTFO > (JWFO UIF QSFTFODF PG DPQB॒FSOT PVS QSPPG TUSVDUVSF JO TPNF XBZT SFTFNCMFT UIBU PG "CFM FU BM <> *U SFRVJSFT B TUBOEBSE TVCTUJUVUJPO MFNNB BT XFMM BT JOWFSTJPO BOE
DBOPOJDBM GPSNT MFNNBTय़BOLT UP UIF QSFTFODF PG FMJNJOBUJPO QB॒FSO NBUDIJOH XF OFFE UP SFBTPO OPU POMZ BCPVU UIFTIBQF PG XFMMUZQFE WBMVFT CVU BMTP XFMMUZQFE FMJNJOBUJPO GSBNFT 'JHVSF  EF੗OFT UZQJOH KVEH
NFOUT GPS FMJNJOBUJPO GSBNFT य़F UZQF 𝐴ˆ PG BO FMJNJOBUJPO GSBNF F JT HJWFO CZ UIF KVEHNFOU
Γ / F ⇒ 𝑉ˆ  "O BMUFSOBUJWF NFUIPE PG UZQJOH FMJNJOBUJPO GSBNFT JT CZ UIJOLJOH PG UIFN BT DPOUFYUT
XIJDI XIFO ੗MMFE XJUI BO FYQSFTTJPO PG UZQF A QSPEVDF BO FYQSFTTJPO PG UZQF B *O UIJT DBTF XF
XSJUF Γ; A / F ⇒ B 8JUI UIFTF EF੗OJUJPOT XF TUBUF PVS DBOPOJDBM GPSNT MFNNB य़JT MFNNBEFTDSJCFT UIF TIBQF PG B WBMVF PS FMJNJOBUJPO GSBNF HJWFO JUT UZQF
-५ॳॳ१  $१ॴॵॴ९३१ॲ 'ॵॸॳॹ  *G · / v ⇐ c A UIFO UIFSF FYJTUT v ( TVDI UIBU v = c v ( *G · / v ⇐ A → B UIFO UIFSF FYJTUT 𝑀 TVDI UIBU v = 𝜆𝑀
 *G · / v ⇐ ∀ 𝛼 .A UIFO UIFSF FYJTUT 𝑀 TVDI UIBU v = 𝜆𝑀 ࡋFSF JT OP v TVDI UIBU · / v ⇐ ⊥
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

/JDL 3JPVY 9VFKJOH )VBOH #SVOP $ E 4 0MJWFJSB BOE 4UFWF ;EBODFXJD

WBMVF UZQFT::=V

Γ / F ⇒ 𝑉ˆc V | 𝐴−

FMJN GSBNF UZQJOH

Γ/v ⇒ VΓ / [·]v ⇒ V

Γ / [·] [A] ⇒ [A]V /A ⇒+ "WBMVF DPWFSBHF

V /A ⇒+ "V /A ⇒+ "c V /c A ⇒+ "V /A % B ⇒+ "V /B ⇒+ "V /A ⇒+ "V /B ⇒+ "V /A % B ⇒+ "V /A # B ⇒+ "−FMJN GSBNF UZQFT𝑉ˆΓ; A / F ⇔ B

FMJN UZQF TZOUIFTJTDIFDLJOH

Γ / F ⇒ 𝑉ˆdisp(A, 𝑉ˆ ) ⇒ B
Γ; A / F ⇒ B

𝑉ˆ /𝐴− ⇒− "::=V | [A]
Γ; A / F ⇒ B (B( ≤ B
Γ; A / F ⇐ B

FMJNJOBUJPO DPWFSBHF

V /A ⇒+ "V /A → B ⇒− "[B]/∀ 𝛼 .A ⇒− "−𝑉ˆ /𝐴−1 ⇒ "−𝑉ˆ /𝐴−2 ⇒ "−𝑉ˆ /𝐴−1 ⇒ "−−𝑉ˆ /𝐴−
1 % 𝐴2 ⇒ "+V /𝐴 ⇒ "−−𝑉ˆ /𝐴−
1 # 𝐴2 ⇒ "−𝑉ˆ /𝐴−2 ⇒ "−−𝑉ˆ /𝐴−
1 # 𝐴2 ⇒ "'JH  %FGJOJUJPOT 6TFE JO 4PVOEOFTT 1SPPG⇒ B UIFO UIFSF FYJTUT v TVDI UIBU F = [·]v
 *G ·; ∀ 𝛼 .A / F ⇒ B UIFO UIFSF FYJTUT C TVDI UIBU F = [·] [C] ࡋFSF BSF OP F BOE B TVDI UIBU ·; , / F ⇒ B*G ·; A → A( / F1ॸॵॵ६ #Z DBTF BOBMZTJT PO UIF WBMVF PS GSBNF JO FBDI QBSU VTJOH QSPQFSUJFT PG TVCUZQJOH

!

8F BMTP IBWF B OVNCFS PG BEEJUJPOBM JOWFSTJPO QSJODJQMFT GPS UIF UZQJOH SFMBUJPO .PTU OPUBCMF
BSF UIPTF GPS VOJPO BOE JOUFSTFDUJPO UZQFT 1FSIBQT TVSQSJTJOHMZ JOWFSTJPO QSJODJQMFT GPS VOSF
TUSJDUFE VOJPO UZQFT SFNBJO BO BDUJWF PCKFDU PG TUVEZ <$BTUBHOB FU BM > (JWFO PVS EJTKPJOUOFTTSFTUSJDUJPOT XF BSF TUSBJHIUGPSXBSEMZ BCMF UP PCUBJO-५ॳॳ१  *G Γ / v ⇐ A1 % A2 BOE A1 ⊳⊲ A2 UIFO Γ / v ⇐ A1 PS Γ / v ⇐ A2 
1ॸॵॵ६ #Z QSPQFSUJFT PG TVCUZQJOH!

य़F EJTUJOHVJTIBCJMJUZ QSFNJTF JT DSVDJBM UP UIJT MFNNB BT JT UIF GBDU UIBU v JT B WBMVF %VBMMZ XF
BMTP IBWF B QSPQFSUZ BCPVU GSBNFT UIBU FMJNJOBUF JOUFSTFDUJPOT PG NFSHFBCMF UZQFT
-५ॳॳ१  4VQQPTF · / A1 # A2  *G ·; A1 # A2 / F ⇒ B UIFO UIFSF FYJTUT B B ( TVDI UIBU FJUIFS·; A1 / F ⇒ B ( PS ·; A2 / F ⇒ B (1ॸॵॵ६ #Z QSPQFSUJFT PG UZQFMFWFM EJTQBUDI!

1SPHSFTT5P QSPWF QSPHSFTT XF NVTU TIPX UIBU FWFSZ DMPTFE XFMMUZQFE UFSN JT FJUIFS B WBMVF PS NBZ UBLF
B TUFQ य़F LFZ DPWFSBHF MFNNB OFFEFE IFSF JT UIBU JG B WBMVF v BOE B QB॒FSO p IBWF UZQF A UIFO
v TIPVME TVDDFTTGVMMZ NBUDI p "O BOBMPHPVT QSPQFSUZ GPS FMJNJOBUJPO GSBNFT BOE FMJNJOBUJPOQB॒FSOT JT BMTP OFFEFE य़FSF BSF B DPVQMF PG JTTVFT 'JSTU A JT OPU OFDFTTBSJMZ UIF QSJODJQBM UZQF PG
v TP DPWFSBHF JT GVOEBNFOUBMMZ B QSPQFSUZ SFMBUJOH TVCUZQJOH UP QB॒FSO NBUDIJOH य़F TVCUZQJOHSFMBUJPO JT SFMBUJWFMZ DPNQMFY TP QSPDFFEJOH EJSFDUMZ CZ JOEVDUJPO PO JU JT USJDLZ 4FDPOE UIF UZQF
A EPFT OPU VOJRVFMZ EFUFSNJOF UIF TIBQF PG UIF QB॒FSO p XIJDI XPVME SFRVJSF B EJSFDU QSPPG UP
BOBMZ[F NBOZ DBTFT
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

" #PXUJF GPS B #FBTU



5P EFBM XJUI UIFTF JTTVFT XF EF੗OF UIF WBMVF DPWFSBHF SFMBUJPO V /A ⇒+ " XIFSF V JT UIFQSJODJQBM UZQF PG B WBMVF BMTP DBMMFE B WBMVF UZQF BOE EFTDSJCFE CZ 'JHVSF  BOE A JT UIF UZQF PG BQB॒FSO य़JT SFMBUJPO IPMET XIFO WBMVFT PG UZQF V NBUDI QB॒FSOT PG UZQF A UIF EF੗OJOH SVMFT PG
UIF SFMBUJPO JO 'JHVSF  DMPTFMZ DPSSFTQPOE UP UIF SVMFT EF੗OJOH UIF QB॒FSO NBUDIJOH QSPDFEVSF
GSPN 'JHVSF  5P BCTUSBDU PWFS FMJNJOBUJPO QB॒FSO NBUDIJOH XF TJNJMBSMZ EF੗OF BO FMJNJOBUJPODPWFSBHF SFMBUJPO 𝑉ˆ /𝐴− ⇒− " )FSF 𝑉ˆ JT UIF UZQF PG BO FMJNJOBUJPO GSBNF य़F NBUDIJOH BCTUSBDUJPO MFNNBT EFTDSJCF UIF JOUFOU CFIJOE CPUI PG UIFTF EF੗OJUJPOT य़BU JT JG B WBMVF‫۝‬T SFTQ FMJNJOBUJPO GSBNF‫۝‬T UZQF NBUDIFT B QB॒FSO‫۝‬T UZQF UIFO UIF WBMVF SFTQ FMJNJOBUJPO GSBNF NBUDIFT UIFQB॒FSO-५ॳॳ१  1१ॺॺ५ॸॴ .१ॺ३८९ॴ७ "२ॹॺॸ१३ॺ९ॵॴ  4VQQPTF · / v ⇒ V BOE · / A *G V /A ⇒+ " UIFO v NBUDIFT BMM QBࡇFSOT p GPS XIJDI UIFSF
FYJTUT TPNF Δ TVDI UIBU · / p ⇒ A 1 Δˆ
 4VQQPTF · / F ⇒ 𝑉ˆ BOE · / 𝑝ˆ ⇒ 𝐵 − ↩→ C 1 Δ *G 𝑉ˆ /𝐵 − ⇒− " UIFO F NBUDIFT 𝑝

1ॸॵॵ६ 'PS UIF ੗STU DBTF QSPDFFE CZ JOEVDUJPO PO V /A ⇒+ " BOE 𝑉ˆ /𝐵 − ⇒− " VTJOH JOWFSTJPOQSPQFSUJFT PG QB॒FSO UZQJOH BOE TVCUZQJOH य़F QSPPG PG UIF TFDPOE DBTF JT BOBMPHPVT!
य़JT MFNNB BMMPXT VT UP SFBTPO BCPVU QB॒FSO NBUDIJOH QVSFMZ BU UIF UZQF MFWFM XF OFFE OPU
XPSSZ BCPVU UIF QBSUJDVMBS WBMVFT PS QB॒FSOT JOWPMWFE *U JT BO BQQSPBDI XJUI B DMFBS DPOOFDUJPOUP BCTUSBDU JOUFSQSFUBUJPO <$PVTPU BOE $PVTPU >
*U SFNBJOT UP DPOOFDU TVCUZQJOH BOE UIF UZQFMFWFM EJTQBUDI PQFSBUPS UP UIF DPWFSBHF SFMBUJPOT-५ॳॳ१  $ॵॳॶॲ५ॺ५ॴ५ॹॹ ॵ६ $ॵॼ५ॸ१७५ 3५ॲ१ॺ९ॵॴॹ  *G V ≤ A UIFO V /A ⇒+ " *G UIFSF FYJTUT C TVDI UIBU disp(𝐴−, 𝑉ˆ ) ⇒ C UIFO 𝑉ˆ /𝐴− ⇒− "

1ॸॵॵ६ #PUI BSF QSPWFE WJB JOEVDUJPO PO UIF QSFNJTF BOE VTF TPNF BVYJMJBSZ MFNNBT UIBU DPOTUSVDU UIF DPWFSBHF SFMBUJPO KVEHNFOUT XIFO POF JOWPMWFE UZQF JT TQMJ॒BCMF य़F QSPPG PG UIF TFDPOE QBSU NBLFT VTF PG UIF ੗STU XIFO 𝐴− JT BO BSSPX UZQF
!
$PWFSBHF OPX GPMMPXT FBTJMZ GSPN UIF QSFWJPVT UXP MFNNBT-५ॳॳ१  $ॵॼ५ॸ१७५  4VQQPTF · / A *G Γ / v ⇐ A BOE Γ / p ⇒ A 1 Δ UIFO v NBUDIFT pˆ *G · / F ⇒ 𝑉ˆ BOE disp(𝐴−, 𝑉ˆ ) ⇒ B1 BOE · / 𝑝ˆ ⇒ 𝐴− ↩→ B2 1 Δ UIFO F NBUDIFT 𝑝

1ॸॵॵ६ 8F QSPWF UIF ੗STU DBTF UIF TFDPOE DBTF GPMMPXT BOBMPHPVTMZ GSPN UIF TBNF MFNNBT#Z UIF EF੗OJUJPO PG Γ / v ⇐ A XF IBWF Γ / v ⇒ V XIFSF V ≤ A #Z -FNNB  XF IBWF
V /A ⇒+ " "QQMZJOH -FNNB  UP UIJT XF IBWF UIBU v NBUDIFT p
!
य़F EFTJSFE QSPHSFTT MFNNB JT B DPOTFRVFODF PG DPWFSBHF

-५ॳॳ१  1ॸॵ७ॸ५ॹॹ  *G · / e ⇒ A UIFO e JT B WBMVF PS UIFSF FYJTUT e ( TVDI UIBU e ↦−→ e (1ॸॵॵ६ #Z JOEVDUJPO PO UIF UZQJOH EFSJWBUJPO GPS e य़F DBTFT GPS FMJNJOBUJPO GPSNT SFMZ VQPO-FNNB !


1SFTFSWBUJPO

8F GBDF B SBUIFS TVCUMF CBSSJFS UP QSPWJOH QSFTFSWBUJPO $POTJEFS UIF XFMMUZQFE BQQMJDBUJPO PG BO
PWFSMPBEFE GVODUJPO UP BO BSHVNFOU
e = 𝜆{(x : Int) ↩→ Int ↦→ e1, (x : Bool) ↩→ Bool ↦→ e2 } v
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

/JDL 3JPVY 9VFKJOH )VBOH #SVOP $ E 4 0MJWFJSB BOE 4UFWF ;EBODFXJD"TTVNJOH · / v ⇒ A BOE x : Int / e1 ⇐ Int BOE x : Bool / e2 ⇐ Bool XF ੗OE UIBU e IBTB UZQF B TVDI UIBU disp((Int → Int) # (Bool → Bool), A) ⇒ B य़F FYQSFTTJPO e SFEVDFT UP UIFFYQSFTTJPO e ( CFMPXe ( = disp({𝑝ˆ1 ↦→ e1, 𝑝ˆ2 ↦→ e2 }, [·]v)&TUBCMJTIJOH UZQF QSFTFSWBUJPO SFRVJSFT TIPXJOH UIBU UIF UZQF PG e ( JT B TVCUZQF PG B य़F QSPCMFN
BSJTFT JO USZJOH UP EFUFSNJOF XIBU B JT य़F UZQFMFWFM EJTQBUDI PQFSBUPS ੗STU TQMJUT UIF UZQF A य़JT
NBLFT UIJOHT EJਖ਼DVMU TJODF UIF POMZ UIJOH XF LOPX BCPVU A JT UIBU JU JT UIF UZQF PG BO BSCJUSBSZWBMVF v *OUVJUJWFMZ JU TFFNT UIBU B TIPVME CF UIF JOUFSTFDUJPO PG UIF PVUQVU UZQF PG FBDI PWFSMPBEUIBU BDDFQUT B BT BO JOQVU 6OGPSUVOBUFMZ UIBU JT OPU BMXBZT USVF 4VQQPTF A = Int % Bool *O UIJT
DBTF A JT B TVCUZQF PG OFJUIFS Int OPS Bool 0O UIF PUIFS IBOE B ≡ Int % Bool य़BOLGVMMZ JU UVSOTPVU UIJT DBTF JT JNQPTTJCMF य़FSF JT OP WBMVF XIPTF QSJODJQBM UZQF JT Int % Bool JU JT OPU B WBMVFUZQF 5P UBLF BEWBOUBHF PG UIJT GBDU XF ੗STU OFFE B DPVQMF PG QSPQFSUJFT SFMFWBOU UP UIF EJTQBUDIQSPDFEVSF
-५ॳॳ१  %ॵॽॴॽ१ॸ४ $ॲॵॹॻॸ५ ॵ६ %९ॹॺ९ॴ७ॻ९ॹ८१२९ॲ९ॺॿ  *G A ⊳⊲ B BOE B ( ≤ B UIFO A ⊳⊲ B (1ॸॵॵ६ *NNFEJBUF GSPN UIF EJTUJOHVJTIBCJMJUZ SVMFT!

-५ॳॳ१  %९ॹॶ१ॺ३८  4VQQPTF splitu (B) " BOE splitu (B () " *G A1 ⊲⊳ A2 BOE disp(A1, B) ⇒ C1
BOE disp(A1, B () " BOE disp(A2, B () ⇒ C2( UIFO B ⊳⊲ B (1ॸॵॵ६ #Z JOEVDUJPO PO A1 ⊲⊳ A2 VTJOH -FNNB !

'SPN UIFTF XF DBO QSPWF UIF SFRVJSFE QSPQFSUJFT PG UIF disp PQFSBUPS-५ॳॳ१  5ॿॶ५ং-५ॼ५ॲ %९ॹॶ१ॺ३८ ॵॴ 7१ॲॻ५ 5ॿॶ५ॹ 
4VQQPTF · / A1 # A2 BOE disp(A1 # A2, 𝑉ˆ ) ⇒ B BOE disp(A1, 𝑉ˆ ) ⇒ B1 
 *G disp(A2, 𝑉ˆ ) ⇒ B2 UIFO B1 # B2 ≤ B
 *G disp(A2, 𝑉ˆ ) " UIFO B1 ≤ B1ॸॵॵ६ #Z TDSVUJOJ[JOH XIFUIFS 𝑉ˆ JT TQMJ॒BCMF BOE BQQMZJOH JOWFSTJPO QSPQFSUJFT PG UIF UZQF
MFWFM EJTQBUDI PQFSBUPS!
य़BOLT UP UIJT MFNNB XF LOPX UIBU XF DBO DPNQVUF UIF PVUQVU UZQF PG BO BQQMJDBUJPO PG BO PWFSMPBEFE GVODUJPO UP BO VOLPXO WBMVF GSPN UIF PVUQVU UZQFT PG FBDI JOEJWJEVBM PWFSMPBE -FNNB 
BMMPXT UIF TVCUZQJOH SFMBUJPOTIJQT JO UIF DPODMVTJPO PG FBDI PG UIFTF DBTFT UP CF TUSFOHUIFOFE UP
BO FRVJWBMFODF
8JUI UIBU EJਖ਼DVMUZ UBLFO DBSF PG XF OFYU UVSO PVS B॒FOUJPO UP UXP LFZ QSPQFSUJFT PG QB॒FSONBUDIJOH य़F ੗STU FOTVSFT UIBU QB॒FSOT PG EJTUJOHVJTIBCMF UZQFT BSF NVUBMMZ FYDMVTJWF XIJMF UIFTFDPOE FOTVSFT UIBU TVCTUJUVUJPOT QSPEVDFE GSPN QB॒FSO NBUDIJOH BSF XFMMUZQFE-५ॳॳ१  %९ॹॺ९ॴ७ॻ९ॹ८१२ॲ५ 1१ॺॺ५ॸॴॹ  4VQQPTF Γ / p1 ⇒ A1 1 Δ1 BOE Γ / p2 ⇒ A2 1 Δ2XIFSF A1 ⊳⊲ A2  ࡋFSF EPFT OPU FYJTU B DMPTFE XFMMUZQFE WBMVF UIBU NBUDIFT CPUI p1 BOE p2 
1ॸॵॵ६ #Z QSPQFSUJFT PG UIF DPWFSBHF SFMBUJPOT BOE JOEVDUJPO PO A1 ⊳⊲ A2 !

-५ॳॳ१  "४५ধ१३ॿ  *G · / p ⇒ A 1 Δ BOE Γ / v ⇐ A BOE v/p ⇒ 𝜎 UIFO Γ / 𝜎 ⇐ Δ 4VQQPTF · / A BOE · / 𝑝ˆ ⇒ A ↩→ B1 1 Δ BOE ·; A / F ⇒ B2 BOE F/𝑝ˆ ⇒ 𝜎 ↩→ B3  ࡋFO·; B1 / 𝜎 ⇐ Δ ↩→ B3 BOE B3 ≤ B2 

1ॸॵॵ६ #Z JOEVDUJPO PO UIF QB॒FSO NBUDIJOH SVMFT VTJOH -FNNB  *O UIF DBTF PG WBMVFQB॒FSO NBUDIJOH BHBJOTU PSQB॒FSOT XF BHBJO NBLF VTF PG -FNNB !
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

" #PXUJF GPS B #FBTUय़F KVEHFNFOU ·; B1 / 𝜎 ⇐ Δ ↩→ B3 JO UIF DPODMVTJPO BCPWF NFBOT ੗STU UIBU FBDI WBMVF JO
𝜎 IBT B UZQF HJWFO CZ Δ BOE TFDPOE UIBU BO FMJNJOBUJPO GSBNF JO 𝜎 IBT JOQVU BOE PVUQVU UZQFT
B1 BOE B3 SFTQFDUJWFMZ 8F SFGFS UIF SFBEFS UP UIF UFDIOJDBM BQQFOEJY <3JPVY FU BM C> GPS JUTGPSNBM EF੗OJUJPO 8JUI BEFRVBDZ FTUBCMJTIFE XF DBO OPX QSPWF UIF UZQF QSFTFSWBUJPO MFNNB-५ॳॳ१  1ॸ५ॹ५ॸॼ१ॺ९ॵॴ  *G · / e ⇐ A BOE e ↦−→ e ( UIFO · / e ( ⇐ A1ॸॵॵ६ #Z JOEVDUJPO PO e ↦−→ e ( NBLJOH VTF PG -FNNB  -FNNB  BOE -FNNB 


!

4PVOEOFTT BOE %FUFSNJOJTN

8JUI QSPHSFTT BOE QSFTFSWBUJPO QSPWFO PVS NBJO SFTVMU JT OPX XJUIJO SFBDI
5८५ॵॸ५ॳ  5ॿॶ५ 4ॵॻॴ४ॴ५ॹॹ  *G · / e ⇐ A BOE e ↦−→∗ e ( UIFO FJUIFS e ( JT B WBMVF PS e ( DBO
UBLF BOPUIFS TUFQ
1ॸॵॵ६ 'PMMPXT GSPN -FNNB  BOE -FNNB  /PUF UIBU e TZOUIFTJ[FT TPNF TVCUZQF PG ACZ UIF EF੗OJUJPO PG UIF DIFDLJOH SFMBUJPO य़VT GVM੗MMJOH UIF QSFNJTF PG UIF QSPHSFTT MFNNB JT OPU
B QSPCMFN!
य़JT FTUBCMJTIFT UIBU XFMMUZQFE QSPHSBNT EP OPU ۠HP XSPOHۡ <.JMOFS > 'VSUIFSNPSF UIFUZQF TZTUFN BMTP FOTVSFT UIF EFUFSNJOJTN PG SFEVDUJPO-५ॳॳ१  %५ॺ५ॸॳ९ॴ९ॹॳ ॵ६ &ॼ१ॲॻ१ॺ९ॵॴ  *G Γ / p ⇒ A 1 Δ BOE Γ / v ⇐ A BOE v/p ⇒ 𝜎1 BOE v/p ⇒ 𝜎2 UIFO 𝜎1 = 𝜎2  *G Γ / 𝑝ˆ ⇒ A ↩→ B 1 Δ BOE Γ / F ⇒ 𝑉ˆ BOE F/𝑝ˆ ⇒ 𝜎1 ↩→ B1 BOE F/𝑝ˆ ⇒ 𝜎2 ↩→ B2 UIFO
𝜎1 = 𝜎2 BOE B1 = B2 
 4VQQPTF · / e ⇒ A *G e ↦−→ e1 BOE e ↦−→ e2 UIFO e1 = e2 1ॸॵॵ६ य़F POMZ TPVSDF PG OPOEFUFSNJOJTN JO UIF EF੗OJUJPO PG QB॒FSO NBUDIJOH BOE SFEVDUJPOJT XIFO p IBT UIF GPSN p1 |p2 XIFSF v NBUDIFT CPUI p1 BOE p2  #Z JOWFSTJPO PO UIF UZQJOH EFSJWBUJPOGPS p1 |p2 UIF UZQF PG p1 NVTU CF EJTUJOHVJTIBCMF GSPN UIBU PG p2  य़JT DPOUSBEJDUT -FNNB  !


3&-"5&% 803,

ࡋF .FSHF 0QFSBUPS BOE %JTKPJOU *OUFSTFDUJPO 5ZQFT 0MJWFJSB FU BM <> QSPQPTFE UIF 𝜆𝑖 DBMDVMVTXIJDI POMZ BMMPXT JOUFSTFDUJPOT PG EJTKPJOU UZQFT य़F HPBM PG UIF EJTKPJOUOFTT SFTUSJDUJPO XBT UP
BEESFTT UIF BNCJHVJUZ JO %VO੗FME‫۝‬T DBMDVMVT BOE QSPWF UIF DPIFSFODF PG UIF FMBCPSBUJPO 7BSJPVTFYUFOTJPOT UP 𝜆𝑖 BT XFMM BT SFMBYBUJPOT UP UIF UZQF TZTUFN XFSF QSPQPTFE BॏFSXBSET #J FU BM
<> SFMBYFE UIF EJTKPJOUOFTT SFTUSJDUJPO SFRVJSJOH JU POMZ PO NFSHFT BOE BMMPXJOH UIF VTF PG
VOSFTUSJDUFE JOUFSTFDUJPOT 5P FOBCMF OFTUFE DPNQPTJUJPO UIFZ BEEFE B NPSF QPXFSGVM TVCUZQJOHSFMBUJPO CBTFE PO UIF XFMMLOPXO #$% TVCUZQJOH <#BSFOESFHU FU BM > SFMBUJPO XIJDI TVQQPSUT
EJTUSJCVUJWJUZ SVMFT GPS JOUFSTFDUJPOT PWFS PUIFS UZQF DPOTUSVDUT)VBOH FU BM <> QSPQPTFE B OFX BQQSPBDI UP NPEFM UIF UZQFEJSFDUFE TFNBOUJDT PG DBMDVMJXJUI B NFSHF PQFSBUPS BMMPXJOH GPS B EJSFDU QSPPG PG EFUFSNJOJTN PG UIF PQFSBUJPOBM TFNBOUJDT3VOUJNF JNQMJDJU VQ DBTUJOH SFQMBDFT DPFSDJWF TVCUZQJOH 'PS FYBNQMF CFJOH BOOPUBUFE CZ BO JOUFSTFDUJPO UZQF A # B NFBOT UIBU B WBMVF XJMM CF DBTU CZ A BOE B SFTQFDUJWFMZ BOE NFSHFE UPHFUIFS
F⊲⊳ BMTP VTFT B UZQFEJSFDUFE TFNBOUJDT CVU JU EPFT OPU FNQMPZ B DBTUJOH SFMBUJPO *OTUFBE PVS EZOBNJD TFNBOUJDT JT CBTFE PO 𝜂FYQBOTJPO "U SVOUJNF NFSHFT BSF SFXSJ॒FO XJUIPVU EVQMJDBUJPOBOE PUIFS BOOPUBUJPOT BSF EJTDBSEFE *O BEEJUJPO VOMJLF BMM QSFWJPVT DBMDVMJ XJUI EJTKPJOU JOUFSTFDUJPO UZQFT F⊲⊳ TVQQPSUT PWFSMPBEJOH BOE VOJPO UZQFT CZ VTJOH UXP NPSF SF੗OFE EJTKPJOUOFTTSFMBUJPOT EJTUJOHVJTIBCJMJUZ BOE NFSHFBCJMJUZ  य़F NFSHFBCJMJUZ SFMBUJPO JO F⊲⊳ JT DMPTFMZ SFMBUFE
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

/JDL 3JPVY 9VFKJOH )VBOH #SVOP $ E 4 0MJWFJSB BOE 4UFWF ;EBODFXJDUP UIF EJTKPJOUOFTT SFMBUJPO JO UIF QSFWJPVT DBMDVMJ "U UIF NPNFOU F⊲⊳ EPFT OPU ZFU TVQQPSU VOSF
TUSJDUFE JOUFSTFDUJPOTVOJPOT BOE EJTKPJOU QPMZNPSQIJTN CVU XF QMBO UP TUVEZ UIFTF FYUFOTJPOT JOUIF GVUVSF
3FटOFNFOU 5ZQFT *OUFSTFDUJPO BOE VOJPO UZQFT BSF VTFE JO SF੗OFNFOU UZQF TZTUFNT UP JODSFBTFUIF UZQFMFWFM FYQSFTTJWFOFTT <%BWJFT BOE 1GFOOJOH  'SFFNBO BOE 1GFOOJOH > 4VDI TZTUFNT FJUIFS EP OPU TVQQPSU PWFSMPBEJOH BT UIFSF JT OP NFSHF PS VTF JU POMZ BT B NFDIBOJTN UP
BOOPUBUF UIF UFSN EJ੖FSFOUMZ <%VO੗FME > य़FTF UZQF TZTUFNT GBDF B TJNJMBS QSPCMFN UIFZ
NVTU DBMDVMBUF UIF SFUVSO UZQF GPS BQQMJDBUJPO XIFSF UIF GVODUJPO DBO IBWF BO JOUFSTFDUJPO PSVOJPO UZQF %VF UP UIF MBDL PG PWFSMPBEJOH UIF TVCUZQJOH SFMBUJPO DBO CF TUSPOHFS BT XF EJTDVTTFEJO g CVU SFEVDUJPO JT UZQF JSSFMFWBOU BOE PॏFO FSBTFT BOOPUBUJPOT0WFSMPBEJOH 4FNBOUJD 4VCUZQJOH BOE $%VDF $BTUBHOB FU BM <> TUVEJFE B SFTUSJDUFE GPSN PG
UIF NFSHF PQFSBUPS GPS PWFSMPBEJOH *O UIFJS DBMDVMVT 𝜆& POMZ NFSHFT PG GVODUJPOT BSF BMMPXFE BOE
POMZ POF GVODUJPO JT TFMFDUFE GPS 𝛽SFEVDUJPO TP OFTUFE DPNQPTJUJPO JT OPU TVQQPSUFE *OTUFBE PG EJTKPJOUOFTT UIF DSJUFSJB JO 𝜆& GPS UZQFT PG NFSHFE GVODUJPOT JT GPS BOZ BSHVNFOU UIBU UIFZ DBO UBLF B
CFTUNBUDIJOH UZQF BMXBZT FYJTUT य़JT SFTUSJDUJPO GPSCJET NFSHJOH B GVODUJPO PG Int → Int → Int
BOE B GVODUJPO PG Int → Bool → Bool CVU JU BMMPXT PWFSMBQQJOH BNPOH PWFSMPBEFE GVODUJPOTXIJDI WJPMBUFT EJTKPJOUOFTT /POFUIFMFTT BEEJOH NPSF JNQMFNFOUBUJPOT UP BO PWFSMPBEFE GVODUJPONBZ MFBE UP B EJ੖FSFOU JNQMFNFOUBUJPO CFJOH DIPPTFO XJUI B CFTUNBUDI TFNBOUJDT XIJDI DPVME
CF VOFYQFDUFE 8JUI EJTKPJOUOFTT UIJT DBOOPU IBQQFO TJODF BEEJOH B OFX PWFSMBQQJOH JNQMFNFOUBUJPO UP BO FYJTUJOH NFSHF XPVME SFTVMU JO B UZQF FSSPSय़F TFNBOUJD TVCUZQJOH <'SJTDI FU BM > BQQSPBDI HJWFT UZQFT B TFUUIFPSFUJD JOUFSQSFUBUJPO$BMDVMJ XJUI TFNBOUJD TVCUZQJOH BSF FRVJQQFE XJUI WFSZ FYQSFTTJWF TVCUZQJOH SFMBUJPOT DPOUBJOJOH VOJPOT JOUFSTFDUJPOT OFHBUJPO UZQFT BOE WBSJPVT EJTUSJCVUJWJUZ SVMFT F⊲⊳ FNQMPZT TZOUBDUJDTVCUZQJOH 8IJMF JUT TVCUZQJOH SFMBUJPO JT RVJUF FYQSFTTJWF JU EPFT OPU TVQQPSU OFHBUJPO UZQFT$BMDVMJ XJUI TFNBOUJD TVCUZQJOH TVQQPSU FYQSFTTJWF GPSNT PG PWFSMPBEJOH XIJDI JT UZQJDBMMZ SFTPMWFE VTJOH B CFTUNBUDI TFNBOUJDT BT JO $BTUBHOB FU BM‫۝‬T XPSL )PXFWFS FYJTUJOH DBMDVMJ XJUITFNBOUJD TVCUZQJOH EP OPU TVQQPSU B NFSHF PQFSBUPS PS OFTUFE DPNQPTJUJPO LFZ GFBUVSFT GPS DPNQPTJUJPOBM QSPHSBNNJOH <;IBOH FU BM > *O DPOUSBTU F⊲⊳ JT EFTJHOFE UP TVQQPSU DPNQPTJUJPOBMQSPHSBNNJOH GFBUVSFT BOE OFTUFE DPNQPTJUJPO JO QBSUJDVMBS *U JOUFHSBUFT GFBUVSFT PG UXP QSFWJPVTMZ TFQBSBUF UZQFT PG DBMDVMJ UIPTF XJUI EJTKPJOU JOUFSTFDUJPO UZQFT BOE UIPTF XJUI PWFSMPBEJOH
$%VDF VTFT TFNBOUJD TVCUZQJOH *UT DPSF DBMDVMVT <9V > IBT B UZQFDBTF FYQSFTTJPO XIJDIIBT UXP CSBODIFT BOE UBLFT BO FYQSFTTJPO XIPTF UZQF BॏFS FWBMVBUJOH UP B WBMVF EFUFSNJOFT
XIJDI CSBODI XJMM CF FYFDVUFE %VF UP JUT TQFDJBM UZQJOH SVMF UIF UZQF DBTF DBO FODPEF PWFSMPBEFEGVODUJPOT UZQFE CZ BO JOUFSTFDUJPO UZQF NBLJOH JU WFSZ TJNJMBS UP EJTKPJOU NFSHFT #VU JU IBT OP
EJTKPJOUOFTT DPOTUSBJOU BOE POMZ DPNQBSFT UIF WBMVF‫۝‬T UZQF BHBJOTU B HJWFO UZQF UIFO CFIBWFT MJLF
B JGUIFOFMTF FYQSFTTJPO य़F DPTU JT GVODUJPOT JO $PSF$%VDF BSF FYQMJDJUMZ BOOPUBUFE *O DPOUSBTUPVS EJTUJOHVJTIBCJMJUZ SFMBUJPO JOUFOUJPOBMMZ BWPJET UIF OFFE GPS DPNQBSJOH B GVODUJPO WBMVF UP B
GVODUJPO UZQF JO UIF SVOUJNF
&MJNJOBUJPO $POTUSVDUT GPS 6OJPO 5ZQFT 6OMJLF TVN UZQFT PS UBHHFE VOJPOT VOUBHHFE VOJPOTBSF OPU BMXBZT FRVJQQFE CZ BO FYQMJDJU FMJNJOBUJPO DPOTUSVDU 8IFO ੗STU JOUSPEVDFE CZ .BDफ़FFOFU BM <> UIF UZQJOH SVMF GPS VOJPO BMMPXT JU UP CF FMJNJOBUFE VOEFS BOZ DPOUFYU UIBU DBO IBOEMF CPUI QPTTJCJMJUJFT PG UIF VOJPO 6OGPSUVOBUFMZ UIJT SVMF CSFBLT UZQF QSFTFSWBUJPO VOMFTT UIF𝛽SFEVDUJPO JT QFSGPSNFE JO QBSBMMFM <#BSCBOFSB FU BM > " TPVOE DBMDVMVT XJUI UIJT UZQJOH SVMF
NVTU BWPJE FWBMVBUJOH UIF UFSN PG B VOJPO UZQF NVMUJQMF UJNFT BॏFS JU TVCTUJUVUFT UIF TBNF WBSJBCMF 5XP LJOET PG SFTUSJDUJPOT BSF FNQMPZFE JO UIF MJUFSBUVSF WBO #BLFM FU BM <> POMZ BMMPXTWBMVFT UP CF UZQFE XJUI VOJPO UZQFT XIJMF %VO੗FME BOE 1GFOOJOH <> UZQFT TVCUFSNT PG VOJPO
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

" #PXUJF GPS B #FBTUUZQF POMZ XIFO UIFZ PDDVS JO BO FWBMVBUJPO DPOUFYU य़F MB॒FS LJOE JT B HFOFSBMJ[BUJPO PG B NPSF
TUSJOHFOU BQQSPBDI FNQMPZFE CZ 1JFSDF <C> UIBU MJNJUT UIF DPOUFYU UP CF B VOJPO FMJNJOBUJPOGPSN'PS UIF BCPWF DBMDVMJ UIF TBNF QJFDF PG DPEF JT FYFDVUFE OP NB॒FS XIBU SVOUJNF UZQF UIF UFSN
IBT #VU QSBDUJDBMMZ NBOZ MBOHVBHFT TVQQPSUJOH VOJPO UZQFT DIPPTF UP IBWF B UZQFEFQFOEFOU
FMJNJOBUJPO DPOTUSVDU *HBSBTIJ BOE /BHJSB <> QSPQPTFE B DBTF BOBMZTJT FYQSFTTJPO GPS 'FBUIFSXFJHIU +BWB 9%VDF IBT B QB॒FSO NBUDIJOH FYQSFTTJPO <)PTPZB BOE 1JFSDF > (FOFSBMMZ
TQFBLJOH UIF FMJNJOBUJPO DPOTUSVDUT JO UIPTF MBOHVBHFT P੖FS B ੗STUNBUDI TFNBOUJDT XIFSF DBTFT
DBO PWFSMBQ BOE SFPSEFSJOH UIF DBTFT NBZ DIBOHF UIF TFNBOUJDT PG UIF QSPHSBN *O F⊲⊳ VOJPOUZQFT BSF FMJNJOBUFE EJSFDUMZ XJUI BQQMJDBUJPOT XIFSF UIF GVODUJPO QBSU DBO CVU EPFT OPU IBWF UP
CF PWFSMPBEFE 0WFSMPBEJOH GVODUJPOT DPNQBSFE UP UZQFDBTF FYQSFTTJPO UZQFE CZ VOJPOT QSPWJEF NPSF QSFDJTF UZQJOH SFTVMUT BT JU DBO EJTDSJNJOBUF UIF BSHVNFOU UZQF 'PS FYBNQMF BQQMZJOH(Int → Int) # (Bool → Bool) UP Int HJWFT VT Int XIJMF UIF DPSSFTQPOEJOH UZQFDBTF XIJDI IBTUZQF (Int % Bool) → (Int % Bool) DBO POMZ HJWFT VT Int % Bool /PUF UIBU UIF JOUFSTFDUJPO UZQF JTB QSPQFS TVCUZQF PG UIF GVODUJPO UZQF XJUI EJTUSJCVUJWJUZ MBXT JO TVCUZQJOH #BTFE PO NBUDIJOHTUZMFT 3FINBO FU BM <>‫۝‬T XPSL JT UIF DMPTFTU UP PVST य़FZ QSPQPTFE B VOJPO FMJNJOBUJPO DPOTUSVDU B TXJUDIDBTF FYQSFTTJPO CBTFE PO EJTKPJOUOFTT य़FJS DPOTUSVDU JT JOTQJSFE CZ UIF $FZMPOMBOHVBHF <,JOH > य़FJS EJTKPJOUOFTT SFMBUJPO JT DMPTFMZ SFMBUFE UP PVS OPUJPO PG EJTUJOHVJTIBCJMJUZ "MUIPVHI UIFJS TZTUFN TVQQPSUT JOUFSTFDUJPO UZQFT JU EPFT OPU IBWF B NFSHF PQFSBUPS BOE
BMM WBMVFT IBWF B QSJODJQBM UZQF UIBU JT OPU BO JOUFSTFDUJPO PS VOJPO XIJDI FMJNJOBUFT NBOZ PG UIFUFDIOJDBM JTTVFT BU UIF DPTU PG TJHOJ੗DBOUMZ MFTT FYQSFTTJWF QPXFS
"$,/08-&%(.&/54
य़JT XPSL IBT CFFO QBSUJBMMZ GVOEFE CZ UIF )POH ,POH 3FTFBSDI (SBOUT $PVODJM QSPKFDUT OVN
CFS   BOE  BOE BMTP TVQQPSUFE CZ UIF /BUJPOBM 4DJFODF 'PVOEBUJPO VO
EFS HSBOU OVNCFS  BOE UIF 0ਖ਼DF PG /BWBM 3FTFBSDI VOEFS HSBOU OVNCFS /
 य़F ੗STU BVUIPS XBT TVQQPSUFE CZ B /4' (SBEVBUF 3FTFBSDI 'FMMPXTIJQ VOEFS HSBOU OVNCFS
 "OZ PQJOJPOT ੗OEJOHT BOE DPODMVTJPOT PS SFDPNNFOEBUJPOT FYQSFTTFE JO UIJT NBUFSJBMBSF UIPTF PG UIF BVUIPST BOE EP OPU OFDFTTBSJMZ SF੘FDU UIF WJFXT PG UIF /4' PS UIF 0/33&'&3&/$&4"OESFBT "CFM #SJHJ॒F 1JFOULB %BWJE य़JCPEFBV BOE "OUPO 4FU[FS  $PQB॒FSOT 1SPHSBNNJOH *O੗OJUF 4USVDUVSFTCZ 0CTFSWBUJPOT *O 1SPDFFEJOHT PG UIF UI "OOVBM "$. 4*(1-"/4*("$5 4ZNQPTJVN PO 1SJODJQMFT PG 1SPHSBNNJOH-BOHVBHFT 3PNF *UBMZ 101- ‫"  ڣ‬TTPDJBUJPO GPS $PNQVUJOH .BDIJOFSZ /FX :PSL /: 64" ۗ
+FBO.BSD "OESFPMJ  -PHJD QSPHSBNNJOH XJUI GPDVTJOH QSPPGT JO MJOFBS MPHJD +PVSOBM PG MPHJD BOE DPNQVUBUJPO   ۗ
'SBODP #BSCBOFSB .BSJBOHJPMB %F[BOJ$JBODBHMJOJ BOE 6HP EF‫۝‬-JHVPSP  *OUFSTFDUJPO BOE 6OJPO 5ZQFT 4ZOUBY BOE
4FNBOUJDT *OGPSNBUJPO BOE $PNQVUBUJPO   +VOF  ۗ)FOL #BSFOESFHU .BSJP $PQQP BOE .BSJBOHJPMB %F[BOJ$JBODBHMJOJ  " ੗MUFS MBNCEB NPEFM BOE UIF DPNQMFUFOFTTPG UZQF BTTJHONFOU ࡋF KPVSOBM PG TZNCPMJD MPHJD    ۗ
9VBO #J BOE #SVOP $ E 4 0MJWFJSB  5ZQFE 'JSTU$MBTT 5SBJUT *O &VSPQFBO $POGFSFODF PO 0CKFDU0SJFOUFE 1SPHSBNNJOH&$001 9VBO #J #SVOP $ E 4 0MJWFJSB BOE 5PN 4DISJKWFST  य़F &TTFODF PG /FTUFE $PNQPTJUJPO *O &VSPQFBO $POGFSFODF PO
0CKFDU0SJFOUFE 1SPHSBNNJOH &$001 
9VBO #J /JOHOJOH 9JF #SVOP $ E 4 0MJWFJSB BOE 5PN 4DISJKWFST  %JTUSJCVUJWF %JTKPJOU 1PMZNPSQIJTN GPS $PNQPTJUJPOBM 1SPHSBNNJOH *O &VSPQFBO 4ZNQPTJVN PO 1SPHSBNNJOH &401 
3JDIBSE #JSE BOE 0FHF EF .PPS  ࡋF "MHFCSB PG 1SPHSBNNJOH 1SFOUJDF)BMM IUUQXXXDTPYBDVLQVCMJDBUJPOTCPPLTBMHFCSB-VDB $BSEFMMJ BOE +PIO $ .JUDIFMM  0QFSBUJPOT PO 3FDPSET *O 1SPDFFEJOHT PG UIF 'JࡄI *OUFSOBUJPOBM $POGFSFODF PO.BUIFNBUJDBM 'PVOEBUJPOT PG 1SPHSBNNJOH 4FNBOUJDT /FX 0SMFBOT -PVJTJBOB 64"  4QSJOHFS7FSMBH #FSMJO )FJEFM
CFSH ۗ
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

/JDL 3JPVY 9VFKJOH )VBOH #SVOP $ E 4 0MJWFJSB BOE 4UFWF ;EBODFXJD+ $BSF॒F 0 ,JTFMZPW BOE $ 4IBO  'JOBMMZ UBHMFTT QBSUJBMMZ FWBMVBUFE 5BHMFTT TUBHFE JOUFSQSFUFST GPS TJNQMFS UZQFEMBOHVBHFT +PVSOBM PG 'VODUJPOBM 1SPHSBNNJOH    ۗ
(JVTFQQF $BTUBHOB  6OJGZJOH 0WFSMPBEJOH BOE 𝜆"CTUSBDUJPO Λ {}  ࡋFPS $PNQVU 4DJ  ۗ BQS  ۗ
(JVTFQQF $BTUBHOB  $PWBSJBODF BOE $POUSPWBSJBODF B GSFTI MPPL BU BO PME JTTVF B QSJNFS JO BEWBODFE UZQF TZTUFNTGPS MFBSOJOH GVODUJPOBM QSPHSBNNFST  -PHJDBM .FUIPET JO $PNQVUFS 4DJFODF 7PMVNF  *TTVF  'FC  (JVTFQQF $BTUBHOB (JPSHJP (IFMMJ BOE (JVTFQQF -POHP  " DBMDVMVT GPS PWFSMPBEFE GVODUJPOT XJUI TVCUZQJOH *OGPSNBUJPO BOE $PNQVUBUJPO   GFC  ۗ
(JVTFQQF $BTUBHOB .JDLB«M -BVSFOU ,JN /HVZ֤O BOE .B॒IFX -VU[F  0O 5ZQF$BTFT 6OJPO &MJNJOBUJPO BOE
0DDVSSFODF 5ZQJOH 1SPD "$. 1SPHSBN -BOH  101- "SUJDMF  +BO   QBHFT"ESJBOB # $PNQBHOPOJ BOE #FOKBNJO $ 1JFSDF  )JHIFSPSEFS JOUFSTFDUJPO UZQFT BOE NVMUJQMF JOIFSJUBODF .BUIFNBUJDBM 4USVDUVSFT JO $PNQVUFS 4DJFODF .4$4    ۗ
8JMMJBN 3 $PPL 8BMUFS )JMM BOE 1FUFS 4 $BOOJOH  *OIFSJUBODF JT /PU 4VCUZQJOH *O 1SPDFFEJOHT PG UIF UI "$.
4*(1-"/4*("$5 4ZNQPTJVN PO 1SJODJQMFT PG 1SPHSBNNJOH -BOHVBHFT 101- ‫"  ڣ‬TTPDJBUJPO GPS $PNQVUJOH .BDIJOFSZ ۗ
.BSJP $PQQP BOE .BSJBOHJPMB %F[BOJ$JBODBHMJOJ  " OFX UZQF BTTJHONFOU GPS 𝜆UFSNT "SDIJW .BUI -PHJL  +BO ۗ
1BUSJDL $PVTPU BOE 3BEIJB $PVTPU  "CTUSBDU *OUFSQSFUBUJPO " 6OJ੗FE -B॒JDF .PEFM GPS 4UBUJD "OBMZTJT PG 1SPHSBNT CZ$POTUSVDUJPO PS "QQSPYJNBUJPO PG 'JYQPJOUT *O 1SPDFFEJOHT PG UIF UI "$. 4*("$54*(1-"/ 4ZNQPTJVN PO 1SJODJQMFT
PG 1SPHSBNNJOH -BOHVBHFT -PT "OHFMFT $BMJGPSOJB 101- ‫"  ڣ‬TTPDJBUJPO GPS $PNQVUJOH .BDIJOFSZ /FX :PSL /:64" ۗ
3PXBO %BWJFT BOE 'SBOL 1GFOOJOH  *OUFSTFDUJPO 5ZQFT BOE $PNQVUBUJPOBM &੖FDUT *O 1SPDFFEJOHT PG UIF 'JࡄI "$.
4*(1-"/ *OUFSOBUJPOBM $POGFSFODF PO 'VODUJPOBM 1SPHSBNNJOH *$'1 ‫"  ڣ‬TTPDJBUJPO GPS $PNQVUJOH .BDIJOFSZ /FX:PSL /: 64" ۗ
+BOB %VO੗FME  "OOPUBUJPOT GPS *OUFSTFDUJPO 5ZQFDIFDLJOH *O 1SPDFFEJOHT PG UIF 4JYUI 8PSLTIPQ PO *OUFSTFDUJPO 5ZQFT
BOE 3FMBUFE 4ZTUFNT &15$4 7PM  4U©QIBOF (SBIBN-FOHSBOE BOE -VDB 1BPMJOJ &ET  ۗ
+BOB %VO੗FME  &MBCPSBUJOH *OUFSTFDUJPO BOE 6OJPO 5ZQFT + 'VODUJPOBM 1SPHSBNNJOH  ۗ  ۗ
+BOB %VO੗FME BOE 'SBOL 1GFOOJOH  5ZQF BTTJHONFOU GPS JOUFSTFDUJPOT BOE VOJPOT JO DBMMCZWBMVF MBOHVBHFT *O*OUFSOBUJPOBM $POGFSFODF PO 'PVOEBUJPOT PG 4PࡄXBSF 4DJFODF BOE $PNQVUBUJPO 4USVDUVSFT 4QSJOHFS ۗ&SJL &SOTU  'BNJMZ 1PMZNPSQIJTN *O &VSPQFBO $POGFSFODF PO 0CKFDU0SJFOUFE 1SPHSBNNJOH &$001 
5JN 'SFFNBO BOE 'SBOL 1GFOOJOH  3F੗OFNFOU UZQFT GPS .- *O 1SPDFFEJOHT PG UIF "$. 4*(1-"/  DPOGFSFODF PO
1SPHSBNNJOH MBOHVBHF EFTJHO BOE JNQMFNFOUBUJPO ۗ
"MBJO 'SJTDI (JVTFQQF $BTUBHOB BOE 7©SPOJRVF #FO[BLFO  4FNBOUJD 4VCUZQJOH %FBMJOH 4FUय़FPSFUJDBMMZ XJUI'VODUJPO 6OJPO *OUFSTFDUJPO BOE /FHBUJPO 5ZQFT + "$.   "SUJDMF  4FQ   QBHFT)BSVP )PTPZB BOE #FOKBNJO $ 1JFSDF  9%VDF " TUBUJDBMMZ UZQFE 9.- QSPDFTTJOH MBOHVBHF "$. 5SBOTBDUJPOT PO*OUFSOFU 5FDIOPMPHZ 50*5    ۗ
9VFKJOH )VBOH BOE #SVOP $ E 4 0MJWFJSB  %JTUSJCVUJOH JOUFSTFDUJPO BOE VOJPO UZQFT XJUI TQMJUT BOE EVBMJUZ GVODUJPOBM QFBSM  1SPDFFEJOHT PG UIF "$. PO 1SPHSBNNJOH -BOHVBHFT  *$'1  ۗ
9VFKJOH )VBOH +JOYV ;IBP BOE #SVOP $ % 4 0MJWFJSB  5BNJOH UIF .FSHF 0QFSBUPS +PVSOBM PG 'VODUJPOBM 1SPHSBNNJOH   "UTVTIJ *HBSBTIJ BOE )JEFTIJ /BHJSB  6OJPO UZQFT GPS PCKFDUPSJFOUFE QSPHSBNNJOH *O 1SPDFFEJOHT PG UIF  "$.
TZNQPTJVN PO "QQMJFE DPNQVUJOH ۗ(BWJO ,JOH  य़F $FZMPO MBOHVBHF TQFDJ੗DBUJPO WFSTJPO  IUUQTDFZMPOMBOHPSHEPDVNFOUBUJPOTQFD%BWJE .BDफ़FFO (PSEPO 1MPULJO BOE 3BWJ 4FUIJ  "O JEFBM NPEFM GPS SFDVSTJWF QPMZNPSQIJD UZQFT *O 1SPDFFEJOHT PG
UIF UI "$. 4*("$54*(1-"/ TZNQPTJVN PO 1SJODJQMFT PG QSPHSBNNJOH MBOHVBHFT ۗ
3PCJO .JMOFS  " य़FPSZ PG 5ZQF 1PMZNPSQIJTN JO 1SPHSBNNJOH + $PNQVU 4ZTUFN 4DJ  "VH  ۗ
.BSUJO 0EFSTLZ 1IJMJQQF "MUIFSS 7JODFOU $SFNFU #VSBL &NJS 4FCBTUJBO .BOFUI 4U©QIBOF .JDIFMPVE /JLPMBZ .JIBZMPW.JDIFM 4DIJO[ &SJL 4UFONBO BOE .B॒IJBT ;FOHFS  "O PWFSWJFX PG UIF 4DBMB QSPHSBNNJOH MBOHVBHF 5FDIOJDBM
3FQPSU &1'-
#SVOP $ E 4 0MJWFJSB BOE 8JMMJBN 3 $PPL  &YUFOTJCJMJUZ GPS UIF .BTTFT *O &VSPQFBO $POGFSFODF PO 0CKFDU0SJFOUFE
1SPHSBNNJOH &$001 #SVOP $ E 4 0MJWFJSB ;IJZVBO 4IJ BOE +P£P "MQVJN  %JTKPJOU JOUFSTFDUJPO UZQFT *O 1SPDFFEJOHT PG UIF TU "$.
4*(1-"/ *OUFSOBUJPOBM $POGFSFODF PO 'VODUJPOBM 1SPHSBNNJOH /FX :PSL /: 64"  *$'1   "TTPDJBUJPOGPS $PNQVUJOH .BDIJOFSZ ۗ
%PNJOJD 0SDIBSE BOE 5PN 4DISJKWFST  )BTLFMM 5ZQF $POTUSBJOUT 6OMFBTIFE *O 1SPDFFEJOHT PG UIF UI *OUFSOBUJPOBM$POGFSFODF PO 'VODUJPOBM BOE -PHJD 1SPHSBNNJOH 4FOEBJ +BQBO '-014‫  ڣ‬4QSJOHFS7FSMBH #FSMJO )FJEFMCFSH ۗ#FOKBNJO $ 1JFSDF B 1SPHSBNNJOH XJUI JOUFSTFDUJPO UZQFT BOE CPVOEFE QPMZNPSQIJTN 1I% %JTTFSUBUJPO $.6$4
 $BSOFHJF .FMMPO 6OJWFSTJUZ
1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 

" #PXUJF GPS B #FBTU#FOKBNJO $ 1JFSDF C 1SPHSBNNJOH XJUI JOUFSTFDUJPO UZQFT VOJPO UZQFT BOE QPMZNPSQIJTN 5FDIOJDBM 3FQPSU(BSSFM 1P॒JOHFS  " UZQF BTTJHONFOU GPS UIF TUSPOHMZ OPSNBMJ[BCMF 𝜆UFSNT 5P )# $VSSZ FTTBZT PO DPNCJOBUPSZ MPHJD
MBNCEB DBMDVMVT BOE GPSNBMJTN  ۗ "DBEFNJD 1SFTT#BCFS 3FINBO 9VFKJOH )VBOH /JOHOJOH 9JF BOE #SVOP $ E 4 0MJWFJSB  6OJPO 5ZQFT XJUI %JTKPJOU 4XJUDIFT *O UI
&VSPQFBO $POGFSFODF PO 0CKFDU0SJFOUFE 1SPHSBNNJOH &$001  +VOF   #FSMJO (FSNBOZ -*1*DT 7PM ,BSJN "MJ BOE +BO 7JUFL &ET +PIO $ 3FZOPMET  1SFMJNJOBSZ EFTJHO PG UIF QSPHSBNNJOH MBOHVBHF 'PSTZUIF 5FDIOJDBM 3FQPSU $.6$4
$BSOFHJF .FMMPO 6OJWFSTJUZ+PIO $ 3FZOPMET  %FTJHO PG UIF 1SPHSBNNJOH -BOHVBHF '034:5)& #JSLIBVTFS #PTUPO *OD 64" ۗ/JDL 3JPVY 9VFKJOH )VBOH #SVOP $ E 4 0MJWFJSB BOE 4UFWF ;EBODFXJD B " #PXUJF GPS B #FBTU "SUJGBDU  IUUQTEPJPSH[FOPEP/JDL 3JPVY 9VFKJOH )VBOH #SVOP $ E 4 0MJWFJSB BOE 4UFWF ;EBODFXJD C " #PXUJF GPS B #FBTU 5FDIOJDBM "QQFOEJY 
5FDIOJDBM 3FQPSU .4$*4 6OJWFSTJUZ PG 1FOOTZMWBOJB5JBSL 3PNQG BOE /BEB "NJO  5ZQF 4PVOEOFTT GPS %FQFOEFOU 0CKFDU 5ZQFT %05  *O 1SPDFFEJOHT PG UIF  "$.
4*(1-"/ *OUFSOBUJPOBM $POGFSFODF PO 0CKFDU0SJFOUFE 1SPHSBNNJOH 4ZTUFNT -BOHVBHFT BOE "QQMJDBUJPOT "NTUFSEBN/FUIFSMBOET 0014-"   "TTPDJBUJPO GPS $PNQVUJOH .BDIJOFSZ ۗ
+FSFNZ ( 4JFL BOE 8BMJE 5BIB  (SBEVBM UZQJOH GPS GVODUJPOBM MBOHVBHFT *O 1SPDFFEJOHT PG UIF 4DIFNF BOE 'VODUJPOBM
1SPHSBNNJOH 8PSLTIPQ 4DIFNF  "$. ۗ
4UF੖FO WBO #BLFM .BSJBOHJPMB %F[BOJ$JBODBHMJOJ 6HP EF‫۝‬-JHVPSP BOE :PLP .PUPIBNB  ࡋF NJOJNBM SFMFWBOU MPHJD
BOE UIF DBMMCZWBMVF MBNCEB DBMDVMVT 5FDIOJDBM 3FQPSU 53"31 य़F "VTUSBMJBO /BUJPOBM 6OJWFSTJUZ
1IJMJQ 8BEMFS  य़F FYQSFTTJPO QSPCMFN +BWBHFOFSJDJUZ NBJMJOH MJTU   IUUQTIPNFQBHFTJOGFEBDVLXBEMFS
QBQFSTFYQSFTTJPOFYQSFTTJPOUYU.JUDIFMM 8BOE  5ZQF *OGFSFODF GPS 3FDPSE $PODBUFOBUJPO BOE .VMUJQMF *OIFSJUBODF *O 4ZNQPTJVN PO -PHJD JO $PNQVUFS 4DJFODF -*$4 ", 8SJHIU BOE . 'FMMFJTFO  " 4ZOUBDUJD "QQSPBDI UP 5ZQF 4PVOEOFTT *OG $PNQVU   /PW  ۗ;IJXV 9V  1BSBNFUSJD 1PMZNPSQIJTN GPS 9.- 1SPDFTTJOH -BOHVBHFT 1I% %JTTFSUBUJPO 6OJWFSTJU© 1BSJT%JEFSPU1BSJT
7**
/PBN ;FJMCFSHFS  'PDVTJOH BOE )JHIFS0SEFS "CTUSBDU 4ZOUBY *O 1SPDFFEJOHT PG UIF UI "OOVBM "$. 4*(1-"/
4*("$5 4ZNQPTJVN PO 1SJODJQMFT PG 1SPHSBNNJOH -BOHVBHFT 4BO 'SBODJTDP $BMJGPSOJB 64" 101- ‫"  ڣ‬TTPDJBUJPOGPS $PNQVUJOH .BDIJOFSZ /FX :PSL /: 64" ۗ
8FJYJO ;IBOH :BP[IV 4VO BOE #SVOP $ E 4 0MJWFJSB  $PNQPTJUJPOBM 1SPHSBNNJOH "$. 5SBOTBDUJPOT PO 1SPHSBNNJOH -BOHVBHFT BOE 4ZTUFNT "QSJM  

1SPD "$. 1SPHSBN -BOH 7PM  /P 101- "SUJDMF  1VCMJDBUJPO EBUF +BOVBSZ 