პროტოტიპური გასწორების e-graph-ები ამატებენ უტოლობას კომპილატორის ოპტიმიზაციაში

კომპილატორის გადაწერები როგორც გასწორება

პროტოტიპი შემოიღებს ჩაშენებულ უტოლობის კავშირს, რომლის სტატუსიც e-graph-ის ფესვურ ტოლობის კავშირთან ახლოსაა. მოტივაცია იმაში მდგომარეობს, რომ კომპილატორის გადაწერები ხშირად მიმართულია: ისინი აბსტრაქტულ ან არასაკმარისად განსაზღვრულ პროგრამას უფრო კონკრეტულ ფორმას უხდებიან, რომელიც მანქანაზე გაშვებადია. წყაროს ენებს შეიძლება შეფასების თანმიმდევრობა გაუსაზღვრავდეს ან მთელი რიცხვის გადავსება და ნულზე გაყოფა ღიდან დარჩეს, რაც ქმნის ოპტიმიზაციისა და თარგმნის შესაძლებლობებს.

წყარო წარმოადგენს პროტოტიპს, რომელიც მაქს უილსის microegg-ის საფუძველზეა შექმნილი, ერთად WASM-ის დემოთი. მისი Python-ის კოდი ტოლობაზე ორიენტირებულ მოდელს უტოლობის union-find ოპერაციებით აფარებს, მათ შორის „ნაკლებია ან ტოლია“ კავშირების დამატების, შემოწმებისა და ჩამონათვლის გზებით.

შეუთავსებელი სქემის შესანავათების მნიშვნელობები

ცენტრალური მაგალითია ციფრულ სქემებში მნიშვნელობა „არ მომარგო“. თუ შესანავათი მხარდაჭერილი არაა, გამოსანავათი შეიძლება ჩავთვალოთ „არ მომარგო“, რაც ოპტიმიზატორს საშუალებას აძლევს აირჩიოს ის შედეგი, რომელიც საუკეთესო სქემას ქმნის. პროტოტიპს შეუძლია ეს მნიშვნელობა ჭეშმარიტებად ან მცდარდებად გასწოროს ისე, რომ მისი გლობალური ტოლობა ცალკე რომელიმესთან არ მოხდეს, რაც ცალკეულ გამოყენებებს დამოუკიდებელი არჩევანის უფლებას აძლევს.

მისი სემანტიკა ტერმინს ლოგიკური მნიშვნელობების ნაკრებთი ასახებს, სადაც „ნაკლებია ან ტოლია“ წერტილობრივ ნაკრების შემცველობას აღნიშნავს. rewrite-le და rewrite-ge წესები მიმართულ გასწორებას მუშავებენ. ამოღების პროცესი შეიძლება ეძებდეს ზემოთ, ქვემოთ ან მხოლოდ ტოლობაზე, იმაზე დამოკიდებული, რომელი გასწორებული ტერმინის ტიპი მოითხოვება.

ცვალებადობა e-graph-ში

კავშირების ფუნქციის სიმბოლოებით გავრცელებისთვის იმპლემენტაცია ინახავს, თუ როგორია თითო არგუმენტი: მონოტონური, ანტიმონოტონური ან არცერთი. მაგალითად გამოიყენება ნაკრებთა განსხვავება: ის პირველ არგუმენტში მონოტონურია, ხოლო მეორეში ანტიმონოტონური. ეს განცხადებები უზრუნველყოფს გასწორების დახურვას, უტოლობის გათვალისწინებით e-matching-ს და ამოღებას.

სქემებს გარდა, წინადადება შესაძლო გამოყენებებად ამოწმებს ლოგიკურ იმპლიკაციას, ურთიერთობათა ალგებრას, ქვეტიპებს, მოთხოვნების შემცველობას და პირველი კლასის განლაგების ანალიზებს. ავტორი გასწორებას სტანდარტული e-graph ცნებების შედარებით პირდაპირი გაფართოებად აღწერს, თუმცა აღნიშნავს კითხვებს უფრო ზუსტი შაბლონის სინტაქსისა და უზედან და ქვედა ურთიერთობის ნაკრებების ალგებრული ხედვის შესახებ.