Վերահաստատման նախատիպային e-graph-երը ավելացնում են հավասարություն կոմպիլյատորի օպտիմիզացիային

Կոմպիլյատորի վերագրումը որպես վերահաստատում

Նախատիպը ներդնում է ներկառուցված հավասարության կապ, որի կարգավիճակը մոտ է e-graph-ի արմատային հավասարության կապին: Դրված է մոտիվացիան՝ կոմպիլյատորի վերագրումները հաճախ ուղղված են աբստրակտ կամ բավարարապետ չսահմանված ծրագրի ավելի կոնկրետ ձևի դեպքին, որը կարող է գործարկվել մեքենայի վրա: Աղբյուրային լեզուները կարող են սահմանել գնահատման հաջորդականություն կամ թողնել ամբողջ թվի գերբեռնումը և զրոյի վրա բաժանումը, ինչը ստեղծում է օպտիմիզացիայի և թարգմանության հնարավորություններ:

Աղբյուրը ներկայացնում է նախատիպ, որը ստեղծված է Max Wills-ի microegg-ի հիմքի վրա՝ միասին WASM-ի ցուցադրությամբ: Նրա Python կոդը հավասարության վրա ուղղված մոդելը ծածկում է հավասարության union-find գործողություններով՝ այդ թվում՝ «ցածր կամ հավասար» կապերի ավելացման, ստուգման և ցուցակավորման ճանապարհնով:

Անհամատեղելի սխեմայի արժեքների իմաստները

Կենտրոնական օրինակը թվային սխեմաներում «չի հասնում» արժեքն է: Եթե անհնարը չի աջակցվում, հնարավորը կարող է դիտվել որպես «չի հասնում», ինչը օպտիմիզատորին թույլ է տալիս ընտրել այն արդյունքը, որը ստեղծում է լավագույն սխեման: Նախատիպը կարող է այս արժեքը ուղղել որպես ճշմարիտ կամ կեղծ այնպես, որ դրա գլոբալ հավասարությունը չլինի որևէ այլ հետ, ինչը առանձին կիրառումներին տալիս է անկախ ընտրության իրավունք:

Նրա սեմանտիկան տերմինը արտապատկերում է տրամաբանական իմաստների հավաքածուն, որտեղ «ցածր կամ հավասար» կետային հավաքածուի պարունակությունը նշանակում է: rewrite-le և rewrite-ge կանոնները մշակում են ուղղված վերագրումը: Հանման գործընթացը կարող է փնտրել վերև, ներքև կամ միայն հավասարության վրա՝ կախված ինչ տեսակի վերագրված տերմին է պահանջվում:

Փոփոխականությունը e-graph-ում

Կապերի ֆունկցիայի սիմվոլներով տարածման համար իրականացումը պահպանում է՝ ինչպես է յուրաքանչյուր արգումենտը՝ մոնոտոն, անտիմոնոտոն կամ ոչ մեկը: Օրինակ՝ օգտագործվում է հավաքածուների տարբերությունը. այն առաջին արգումենտում մոնոտոն է, իսկ երկրորդում՝ անտիմոնոտոն: Այս հայտարարությունները ապահովում են վերագրման փակումը, հավասարությունը հաշվի առնելով e-matching-ը և հանումը:

Սխեմաներից բացի, նախադասությունը որպես հնարավոր կիրառումներ ստուգում է տրամաբանական իմպլիկացիան, հարաբերությունների ալգեբրան, ենթատեսակները, պահանջների պարունակությունը և առաջին դասի դասավորության վերլուծությունները: Հեղինակը վերագրումը ստանդարտ e-graph հասկացությունների համեմատ անմիջապես ընդլայնելի է նկարագրում, սակայն նշում է հարցեր ավելի ճշգրիտ շաբլոնի շարահյուսության և վերին և ստորին հարաբերությունների հավաքածուների ալգեբրային տեսության մասին: