{title= Ϩίʔυ‫ࢉܭ‬ͷଟ૬‫ܕ‬γεςϜͱ‫ܕ‬ਪ࿦ ,author=date=@bd_gfngfn

೥݄೔,}ࠓճѻ͏࿦จ
• A. Ohori.

A Polymorphic record calculus andits compilation, 1995.

• E. Osinski. A Polymorphic Type System andCompilation Scheme
for Record Concatenation, 2006.

ࠓճѻ͏࿦จ
• A. Ohori.

A Polymorphic record calculus andits compilation, 1995.

• E. Osinski. A Polymorphic Type System andCompilation Schemeʢਖ਼௚ͳͱ͜Ζؒʹ߹͍·ͤΜͰͨ͠ʣfor Record Concatenation, 2006.

લऀʹয఺Λ౰ͯͯઆ໌ɼ‫ऀޙ‬͸͘͝ॳาΛ঺հϨίʔυͱ͸௚‫؍‬తʹ͸ɿ• ֤ཁૉʹϥϕϧ͕͍ͭͨλϓϧ• ͍ΘΏΔ keyval ΍ dictionaryɼ࿈૝഑ྻʹࣅ͍ͯΔʢͨͩ͠ϥϕϧ໊͸จࣈྻ஋Ͱ͸ͳࣝ͘ผࢠతʹѻ͏ʣ

{foo= 42, bar= true}Ϩίʔυʹର͢ΔԋࢉͱΓ͋͑ͣ‫ܕ‬Λ౓֎ࢹ͢Δͱͯ͠ɼॻ͚Δͱ‫࡞ૢͳ͏ͦ͠خ‬͸ɿ• “ୈ1‫ߏ ”ͳڃ‬ஙʢ͜Ε͸ॻ͚ͯ౰વʣ
let r = {foo= 42, bar= true} in · · ·• ϑΟʔϧυऔग़͠ʢ͜Ε΋౰વʣr foo• ߋ৽r update bar false

42{foo= 42, bar= false}※ “஋Λ෴͍Ӆ͍ͯ͠Δ” ͚ͩͰɼഁյత୅ೖͰ͸ͳ͍Ϩίʔυʹର͢Δԋࢉ• ֦ு{foo= 42} extend bar true

{foo= 42, bar= true}‫·ؚʹط‬ΕΔϥϕϧͱඃΔ৔߹ɼ্ॻ͖͢Δ͔Կ΋͠ͳ͍͔Ͱ
ϰΝϦΤʔγϣϯ͋Γ• ࿈઀ (concatenation){foo= 42, bar= true} |&| {foo= 0, baz= “ Φο ”}{foo= 0, bar= true, baz= “ Φο ”}ϥϕϧ͕ॏෳ͢Δ৔߹Λ‫ऀޙͯ͠ڐ‬ͷ஋Λ༏ઌ͢Δ΋ͷͱ‫͍ͳ͞ڐ‬΋ͷͱͷϰΝϦΤʔγϣϯ͋Γλϓϧʹൺ΂ͨϨίʔυͷ͋Γ͕ͨΈ• ϥϕϧͷ͓͔͛Ͱ୯७ʹίʔυͷυΩϡϝϯτੑ͕޲্λϓϧྲྀ(“realDonaldTrump”, “Donald J. Trump”, true, true)λϓϧʹൺ΂ͨϨίʔυͷ͋Γ͕ͨΈ• ϥϕϧͷ͓͔͛Ͱ୯७ʹίʔυͷυΩϡϝϯτੑ͕޲্λϓϧྲྀ(“realDonaldTrump”, “Donald J. Trump”, true, true)Ϩίʔυྲྀ{screen_name= “realDonaldTrump”,name= “Donald J. Trump”,
is_official= true, is_public= true}λϓϧʹൺ΂ͨϨίʔυͷ͋Γ͕ͨΈ• “ଟ૬ੑ” Λ࣋ͪɼͦͷ͏͑ “૊ʹͯ͠ѻ͏ཁૉ” ͷ࢓༷มߋʹରͯ͠΋ίʔυ͕‫ڧؤ‬

let send_missile = ⁄account.

૊ͷཁૉͷ࢓༷มߋͷͨͼʹॻ͖‫͑׵‬Δඞཁ͋Γ

let (screen_name, _, _, _) = account in
send_reply screen_name “🚀 ”
let send_missile = ⁄account.
send_reply (account screen_name) “🚀 ”໰୊ҙࣝ• ‫ͱͩ͠ͳܕ‬ʢ౰વͳ͕Βʣऔग़͠ͳͲͷࡍʹࣦഊ͠͏Δ{foo= 42} bar

ɾ@ɾAഁ໓ద੾ͳ‫ܕ‬γεςϜΛઃ‫ͯ͠ܭ‬ɼࣦഊ͠ಘͳ͍ϓϩάϥϜʹ͚ͩ੩తʹ‫͕ͭ͘ܕ‬Α͏ʹ͍ͨͨͩ͠͠ɼͦͷࡍʹ……

໰୊ҙࣝ• Ͱ͖Δ͚ͩอकతʹͳΓ͗͢ͳ͍Α͏ʹ͍ͨ͠ʢલड़ͷԋࢉͷͳΔ΂͘ଟ͘Λ “ࣗવͳൣғͰ”αϙʔτ͍ͨ͠ʣ• ओཁ‫( ܕ‬principal type) ͕ଘࡏ͠ɼ͔ͭͦΕ͕‫ܕ‬ਪ࿦ͰಘΒΕΔମ‫͍ͨ͠ʹܥ‬• Ͱ͖Ε͹ΑΓ‫཰ޮ্ࢉܭ‬తͳ‫ͱ΁ࣜܗ‬ίϯύΠϧͰ͖ΔΑ͏ʹ͍ͨ͠

<0IPSJ>֓ཁ
• SML# ͷ‫ܕ‬γεςϜͷ‫͚ͮૅج‬• ૒ରͰ͋Δଟ૬ϰΝϦΞϯτ΋αϙʔτʢࠓճ͸ѻΘͳ͍ʣ• Ұൠతͳେ͖͍ೖྗʹରͯ͠΋े෼ߴ଎ʹ‫ܕ‬ਪ࿦͕ಈ࡞✴ Ϩίʔυͷ֦ு΍࿈઀͸αϙʔτ͠ͳ͍✓ ‫ܕ‬ਪ࿦Մೳ✓ ίϯύΠϧʹΑΔޮ཰Խ͕Մೳ✓ ʢओ‫͕ͳ؍‬Βʣਪ࿦͞ΕΔ‫͕ܕ‬ൺֱతΘ͔Γ΍͍͢

<0TJOTLJ>֓ཁ
• ത࢜࿦จʢಉஶऀ།Ұͷ publication Β͍͠ʁʣ✓ લड़ͷ͢΂ͯͷԋࢉΛαϙʔτ✓ ‫ܕ‬ਪ࿦Մೳ✓ ίϯύΠϧʹΑΔޮ཰Խ͕Մೳ˛ ʢओ‫͕ͳ؍‬Βʣਪ࿦͞ΕΔ‫͕ܕ‬ෳࡶͰΘ͔Γʹ͍͘ʁ˛ ࣮૷͕·ͩແ͍Α͏Ͱɼ࣮࣌ؒͷಈ࡞ʹ‫͑ת‬Δ͔ෆ໌ʢࣗ෼ͷखͰ࣮૷͔ͯ֬͠ΊΔͭ΋ΓͰ͕ͨؒ͠ʹ߹Θͣʣߏ੒•എ‫ܠ‬•͓͞Β͍ɿLetଟ૬ͷ‫ܕ‬ਪ࿦
•[Ohori 1995]•[Osinski 2006]•·ͱΊ߲ͱ‫ܕ‬‫ܕ‬Ḽऍͳ͠ͷ߲Λओͱͯ͠࢖༻•஋•߲

v ····= c | ⁄x. ee ····= v | x | e e | let x = e in e࣮༻্͸ෆಈ఺ (fix x. ⁄x. e) ΍৚݅෼‫ ذ‬if e then e else e΋ඞཁ͕ͩɼ؆୯ͷͨΊࠓճ͸‫ؚ‬Ίͳ͍• ୯૬‫ܕ‬• ଟ૬‫ܕ‬· ····= b | – | · æ ·‡ ····= · | ’–. ‡‫ن͚ͭܕ‬ଇ≈ „e:·‫ܕ‬ม਺ͷଋറग़‫ݱ‬ͷ“ΠϯελϯεԽ”(‡ :© ≈ (x ), ‡ > · )≈ [x ‘æ · Õ ] „ e : ·≈ „ (⁄x. e) : · Õ æ ·≈ „x:·≈ „ e1 : · Õ æ ·≈ „ e2 : · Õ≈ „ e1 e2 : ·≈ „ e1 : ·1‫ܕ‬ม਺ͷྔԽ(‡ :© Gen(≈, · ))≈ [x ‘æ ‡ ] „ e2 : ·2

≈ „ let x = e1 in e2 : ·2‫ن͚ͭܕ‬ଇͷಡΈํ
1. ७ਮʹ3߲ؔ܎ͷ‫ؼ‬ೲతఆٛͱͯ͠≈ „ e1 : · Õ æ ·≈ „ e2 : · Õ “Ծఆଆ”“‫݁ؼ‬ଆ”≈ „ e1 e2 : ·2. ΞϧΰϦζϜͱͯ͠ɿ “Լ͔ΒಡΉ”≈ „ e1 : · Õ æ ·≈ „ e2 : · Õ≈ „ e1 e2 : ·‫ن͚ͭܕ‬ଇͷಡΈํ
1. ७ਮʹ3߲ؔ܎ͷ‫ؼ‬ೲతఆٛͱͯ͠≈ „ e1 : · Õ æ ·≈ „ e2 : · Õ “Ծఆଆ”“‫݁ؼ‬ଆ”≈ „ e1 e2 : ·2. ΞϧΰϦζϜͱͯ͠ɿ “Լ͔ΒಡΉ”≈ „ e1 : · Õ æ ·≈ „ e2 : · Õ≈ „ e1 e2 : ·‫ن͚ͭܕ‬ଇͷಡΈํ
1. ७ਮʹ3߲ؔ܎ͷ‫ؼ‬ೲతఆٛͱͯ͠≈ „ e1 : · Õ æ ·≈ „ e2 : · Õ “Ծఆଆ”“‫݁ؼ‬ଆ”≈ „ e1 e2 : ·2. ΞϧΰϦζϜͱͯ͠ɿ “Լ͔ΒಡΉ”≈ „ e1 : · Õ æ ·≈ „ e2 : · Õ≈ „ e1 e2 : ·‫ن͚ͭܕ‬ଇͷಡΈํ1. ७ਮʹ3߲ؔ܎ͷ‫ؼ‬ೲతఆٛͱͯ͠≈ „ e1 : · Õ æ ·≈ „ e2 : · Õ “Ծఆଆ”“‫݁ؼ‬ଆ”≈ „ e1 e2 : ·2. ΞϧΰϦζϜͱͯ͠ɿ “Լ͔ΒಡΉ”≈ „ e1 : · Õ æ ·≈ „ e2 : · Õ≈ „ e1 e2 : ·‫ن͚ͭܕ‬ଇͷಡΈํ
1. ७ਮʹ3߲ؔ܎ͷ‫ؼ‬ೲతఆٛͱͯ͠≈ „ e1 : · Õ æ ·≈ „ e2 : · Õ “Ծఆଆ”“‫݁ؼ‬ଆ”≈ „ e1 e2 : ·2. ΞϧΰϦζϜͱͯ͠ɿ “Լ͔ΒಡΉ”≈ „ e1 : · Õ æ ·≈ „ e2 : · Õ≈ „ e1 e2 : ·‫ن͚ͭܕ‬ଇͷಡΈํ
1. ७ਮʹ3߲ؔ܎ͷ‫ؼ‬ೲతఆٛͱͯ͠≈ „ e1 : · Õ æ ·≈ „ e2 : · Õ “Ծఆଆ”“‫݁ؼ‬ଆ”≈ „ e1 e2 : ·2. ΞϧΰϦζϜͱͯ͠ɿ “Լ͔ΒಡΉ”≈ „ e1 : · Õ æ ·≈ „ e2 : · Õ≈ „ e1 e2 : ·ʢ˞ෆਖ਼֬ɼ͋͘·Ͱ௚‫؍‬ʣ‫ن͚ͭܕ‬ଇ͔Β‫ܕ‬ਪ࿦ΞϧΰϦζϜ΁‫ܕ‬ਪ࿦ΞϧΰϦζϜͱͯ͠͸ɼΑΓਖ਼֬ʹ͸‫ܕ‬ม਺ͱ୅ೖʢ‫ܕ‬ม਺Λ࣮ࡍͷ‫ؔ΁ܕ‬࿈͚ͮΔ෦෼ࣸ૾ʣΛ࢖͏
ͭ·Δͱ͜Ζ‫ܕ‬ਪ࿦ͱ͸ʮະ஌ͷ‫ܕ‬Λ‫ܕ‬ม਺Ͱஔ͍͓͖ͯɼ߲Λ૸ࠪͯ͠छʑͷ੍໿Λ΋ͱʹ୅ೖΛҭ͍ͯͯ͘ʯॲཧ੍໿ͷղফ݁Ռͱͯ͠ԼΓ͖ͯͨ୅ೖ‫͕ܕ‬ະ஌ͷͱ͜ΖΛ‫ܕ‬ม਺Ͱஔ্͍ͯΔ(– fresh)≈ [x ‘æ – ] „ e : · ¿ ◊≈ „ (⁄x. e) : (◊– æ · ) ¿ ◊ԼΓ͖ͯͨ୅ೖΛ࢖࣮ͬͯࡍͷ‫ܕ‬ΛಘΔ‫ن͚ͭܕ‬ଇ͔Β‫ܕ‬ਪ࿦ΞϧΰϦζϜ΁୯ҰԽɿ≈ „ e1 : ·1 ¿ ◊1◊1 ≈ „ e2 : ·2 ¿ ◊2?
Õ ·– fresh◊ ·= Unify({◊2 ·1 = ·2 æ – }),≈ „ e1 e2 : ◊Õ – ¿ ◊Õ ¶ ◊2 ¶ ◊1‫ܕ‬ͷ౳੍ࣜ໿Λղ͍ͯ୅ೖʹ͢Δॲཧɼ‫ܕ‬ਪ࿦ͷࠜ‫װ‬୯ҰԽ
Unify(E ) ͕‫ݺ‬͹ΕͨΒɼ(E, ?) ͔ΒҎԼͷॻ͖‫͑׵‬Λ࢝Ίɼ(?, ◊) ͷ‫ʹܗ‬౸ୡͨ͠Βͦͷ ◊ Λฦ్͢தͰॻ͖‫͑׵‬ΒΕͳ͘ͳͬͨΒॆ଍ෆՄೳʢ‫ܕ‬Τϥʔ૬౰ʣ?

(E ‡ {· = · }, ◊) ≠æ (E, ◊)?
(E ‡ {· = – }) ≠æ ([· /–]E, {– ‘æ · } ¶ ◊)(if – ”œ FTV(· ))(E ‡ {?

·1 æ ·2 = ·1Õ æ ·2Õ}, ◊) ≠æ (E ﬁ {?

? ÕÕ
·1 = ·1 , ·2 = ·2}, ◊)ߏ੒•എ‫ܠ‬•͓͞Β͍ɿLetଟ૬ͷ‫ܕ‬ਪ࿦
•[Ohori 1995]•[Osinski 2006]•·ͱΊ‫ػ‬ೳ໘ͷ֓ཁʢ࠶‫ܝ‬ʣ• SML# ͷ‫ܕ‬γεςϜͷ‫͚ͮૅج‬• ૒ରͰ͋Δଟ૬ϰΝϦΞϯτ΋αϙʔτʢࠓճ͸ѻΘͳ͍ʣ• Ұൠతͳೖྗʹରͯ͠े෼ߴ଎ʹ‫ܕ‬ਪ࿦͕ಈ࡞✴ Ϩίʔυͷ֦ு΍࿈઀͸αϙʔτ͠ͳ͍✓ ‫ܕ‬ਪ࿦Մೳ
✓ ίϯύΠϧʹΑΔޮ཰Խ͕Մೳ✓ ʢ΍΍ओ‫͕ͳ؍‬Βʣਪ࿦͞ΕΔ‫͕ܕ‬ൺֱతΘ͔Γ΍͍͢ཧ࿦໘ͷ֓ཁ• ‫ܕ‬γεςϜɿ• ༗քྔԽʹΑΔଟ૬• ‫ܕ‬ͷؒͷ෦෼‫< ܎ؔܕ‬: ͸ཅʹ͸ѻΘͣɼछ (kind) ͷ‫Ͱܗ‬ද‫͢ݱ‬Δ• ‫ܕ‬ਪ࿦ɿ• Letଟ૬ͷ‫ܕ‬ਪ࿦Ͱ࢖ΘΕΔ௨ৗͷ୯ҰԽΛ“छͷ੍໿ղফͱฒߦͯ͠ߦ͏୯ҰԽ” ΁ͱมߋ࣮ͯ͠‫ݱ‬߲ͷఆٛͷ֦ு•஋•߲

v ····= c | ⁄x. e | {¸= v, . . . , ¸= v}
e ····= v | x | e e | let x = e in e

| {¸= e, . . . , ¸= e} | e ¸ | e update ¸ eϑΟʔϧυऔΓग़͠ϑΟʔϧυߋ৽‫͚ͭܕ‬ͷͨΊͷߟ࡯ҎԼͷവ਺ʹͲΜͳ‫ܕ‬Λ͚ͭΕ͹Αͦ͞͏͔ʁ

let send_missile = ⁄account.
send_reply (account screen_name) “🚀 ”
screen_nameaccount ͸ɼɹɹɹɹɹɹɹͷϑΟʔϧυ͕Ҿ਺ɹɹɹɹ
จࣈྻ஋ͱͯ͠࢖ΘΕ͍ͯΔͷΈ{screen_name=, . . .}ɹɹɹɹɹɹɹɹʢจࣈྻ஋ʣɹɹɹͷ‫ܗ‬ͷ஋͸શ෦ड͚औͬͯΑ͍ɼ͜ΕΛ൓өͨ͠‫ܕ‬Λ͚ͭΔ

‫ͱܕ‬छʀ֊ͷମ‫ܥ‬• ୯૬‫ܕ‬· ····= b | – | · æ · | {¸ : · , . . . , ¸ : · }• ଟ૬‫ܕ‬‡ ····= · | ’– :: Ÿ. ‡•छŸ ····= U | {{¸ : · , . . . , ¸ : · }}छʹΑΔ “੍໿”͖ͭͷྔԽ’– :: U. ‡ ͕ैདྷͷɹɹɹ’–. ‡ ʹ૬౰ʢͭ·Γ “੍໿” ͳ͠ʣ{{¸1 : ·1 , . . . , ¸n : ·n }} ͸௚‫؍‬తʹ͸Ϩίʔυछɹɹɹɹɹɹɹɹɹɹ

ʮগͳ͘ͱ΋֤ ¸i : ·i ͸શ෦‫ؚ‬ΉϨίʔυ‫ܕ‬શମʯΛࢦ͢Ϩίʔυछͷ௚‫؍‬ྫ{foo : int} :: {{foo : int}}{foo : int, bar : bool} :: {{foo : int}}{foo : int, bar : bool, baz : string} :: {{foo : int}}ྫ{foo : int, bar : bool} :: {{foo : int, bar : bool}}{foo : int, bar : bool,baz : string} :: {{foo : int, bar : bool}}‫͚ͭܕ‬ͷྫ
let send_missile = ⁄account.
send_reply (account screen_name) “🚀 ”account ͷ‫ܕ‬͸ · :: {{screen_name : string}}Ҿ਺ɹɹɹɹ
ͳΔ೚ҙͷ · ͰΑ͍

send_missile ʹ͚ͭΔ‫ܕ‬͸’– :: {{screen_name : string}}. – æ unitྔԽʹؔ͢Δए‫ׯ‬ͷ஫ҙ௨ৗͷLetଟ૬ͱҧ͍ɼྔԽͷॱ൪΋ҙຯΛ࣋ͭ

let get_name = ⁄x. x nameget_nameɹʹͭ͘‫ܕ‬͸’— :: U. ’– :: {{name : — }}. – æ —Ͱ͋ͬͯ’– :: {{name : — }}. ’— :: U. – æ —Ͱ͸ͳ͍ଋറ͞Ε͍ͯͳ͍ग़‫ݱ‬‫ن͚ͭܕ‬ଇͷͨΊͷछ‫ڥ؀‬ͷಋೖछ‫ ڥ؀‬K ɿ‫ܕ‬ม਺ʹछΛؔ࿈͚ͮΔ෦෼ࣸ૾

K : – ‘≠æ Ÿcf. ‫ ≈ ڥ؀ܕ‬ɿม਺ʹ‫ܕ‬Λؔ࿈͚ͮΔ෦෼ࣸ૾߲

‫ܕ‬छe‡

Ÿææ
≈
K≠‘≠
‘
–x‫ن͚ͭܕ‬ଇʢൈਮʣ
· ͸K|≈ „e:·“छ‫ ڥ؀‬K ͷԼͰɼ‡ ͷΠϯελϯεͰ͋Δ”ʢ‫ࣜܗ‬Խ͸ෳࡶͳͷͰׂѪʣ(‡ © ≈ (x ),K „ ‡ > ·)K|≈ „x:·K | ≈ „ ei : ·i (for each i)
K | ≈ „ {¸1 = e1 , . . . , ¸n = en } : {¸1 : ·1 , . . . , ¸n : ·n }‫ن͚ͭܕ‬ଇʢൈਮʣ
K|≈ „e:·“छ‫ ڥ؀‬K ͷԼͰ· ʹछ {{¸ɹ: · Õ }} ͕ͭ͘”K|≈ „e:·K „ · :: {{¸ : · }}K | ≈ „ (e ¸) : · ÕÕK|≈ „e:·K|≈ „e :·K „ · :: {{¸ : · }}K | ≈ „ (e update ¸ eÕ ) : ·ÕÕÕ‫ن͚ͭܕ‬ଇʢൈਮʣ
K|≈ „e:·“छ‫ ڥ؀‬K ͷԼͰ· ʹछ {{¸ɹ: · Õ }} ͕ͭ͘”K|≈ „e:·K „ · :: {{¸ : · }}K | ≈ „ (e ¸) : · ÕÕK „ {R} :: {{RÕ }}:≈∆ R ´ RÕK „ – :: {{RÕ }}:≈∆ R ´ RÕ({{R}} :© K (– ))K|≈ „e:·K|≈ „e :·K „ · :: {{¸ : · }}K | ≈ „ (e update ¸ eÕ ) : ·ÕÕÕ‫҆ܕ‬શੑ஋‫ͼݺ‬ઓུͰ͸ɼ‫·ࢭ͕ࢉܭ‬Δͱ͖͸ඞͣ஋ʹͳ͍ͬͯΔɿఆཧ

? | ? „ e : · ͔ͭ e » e ͳΒ͹ɼe ͸ · ‫ܕ‬ͷ஋Ͱ͋ΔɽÕÕ஋‫ͼݺ‬ઓུͰ؆໿Ͱ͖ͳ͘ͳΔ·Ͱ؆໿͠ଓ͚Δূ໌͸࿦ཧؔ܎ (logical relation) ͷख๏ʹΑΔ‫ن͚ͭܕ‬ଇ͔Β‫ܕ‬ਪ࿦ΞϧΰϦζϜ΁͜ͷମ‫ܥ‬ͷ‫ܕ‬ਪ࿦Ͱ͸ɼ୅ೖͱ‫ʹڞ‬छ‫ڥ؀‬΋߱Γͯ͘Δʢͭ·Γछ‫ڥ؀‬΋‫ܕ‬ม਺ʹର͢Δ੍໿ͷղফ݁Ռʣ

K [– ‘æ U] | ≈ [x ‘æ – ] „ e : · ¿ K Õ | ◊Õ
K | ≈ „ (⁄x. e) : (◊– æ · ) ¿ K | ◊(– fresh)K | ≈ „ e1 : ·1 ¿ K1 | ◊1(—1 , — fresh)?
Õ Õ ·(K , ◊ ) ·= Unify(K1 [— ‘æ U][—1 ‘æ {{¸ : — }}], {·1 = —1 })K | ≈ „ (e1 ¸) : ◊Õ — ¿ K Õ | ◊Õ ¶ ◊1छΛՃຯͨ͠୯ҰԽʢൈਮʣ
(K, E ‡ {–1 = –2 }, ◊) ≠æ (K , E , ◊ )?

ÕÕÕwhereछΛ “߹ซ”ͤ͞Δ྆‫ܕ‬ม਺ͷ{{R1 }} :© K (–1 )ʢॏෳ͢Δ෦෼͸Ұํ͚ͩʣ‫ࡏݱ‬ͷछ
{{R2 }} :© K (–2 )Õ ·K ·= ([–2 /–1 ]K )[–1 ‘æ [–2 /–1 ]{{R1 ﬁ R2 }}]?
Õ ·E ·= [–2 /–1 ](E ﬁ {R1 (¸ ) = R2 (¸ ) | ¸ œ dom R1 ﬂ dom R2 })◊Õ ··= ([–2 /–1 ]◊)[–1 ‘æ –2 ]ϥϕϧ͕ॏෳ͢Δ෦෼͸ಉҰͷ‫͍ͳ͚͍ͱ͍ͳͰܕ‬छΛՃຯͨ͠୯ҰԽʢൈਮʣ
(K, E ‡ {– = {R}}, ◊) ≠æ (K , E , ◊ )
?

ÕÕ

Õ

if dom RÕ ™ dom R and – ”œ FTV({R})
where‫ܕ‬ม਺ͷ‫ࡏݱ‬ͷछ
{{RÕ }} :© K (– )
Õ ·K ·= [{R}/–]K?
ÕÕ ·E ·= [{R}/–](E ﬁ {R (¸ ) = R(¸ ) | ¸ œ dom RÕ })Õ ·◊ ·= ([{R}/–]◊)[– ‘æ {R}]ϥϕϧ͕ॏෳ͢Δ෦෼͸ಉҰͷ‫͍ͳ͚͍ͱ͍ͳͰܕ‬ߏ੒•എ‫ܠ‬•͓͞Β͍ɿLetଟ૬ͷ‫ܕ‬ਪ࿦
•[Ohori 1995]•[Osinski 2006]•·ͱΊ‫ػ‬ೳ໘ͷ֓ཁʢ࠶‫ܝ‬ʣ• ത࢜࿦จʢಉஶऀ།Ұͷ publication Β͍͠ʁʣ✓ લड़ͷ͢΂ͯͷԋࢉΛαϙʔτ✓ ‫ܕ‬ਪ࿦Մೳ✓ ίϯύΠϧʹΑΔޮ཰Խ͕Մೳ˛ ʢओ‫͕ͳ؍‬Βʣਪ࿦͞ΕΔ‫͕ܕ‬ෳࡶͰΘ͔Γʹ͍͘ʁ˛ ࣮૷͕·ͩແ͍Α͏Ͱɼ࣮࣌ؒͷಈ࡞ʹ‫͑ת‬Δ͔ෆ໌ʢࣗ෼ͷखͰ࣮૷͔ͯ֬͠ΊΔͭ΋ΓͰ͕ͨؒ͠ʹ߹Θͣʣཧ࿦໘ͷ֓ཁ• ࣭Խ‫( ܕ‬qualified type) Λ౔୆ͱ͍ͯ͠Δɿ

’X. P ∆ ·‫ܕ‬ม਺ͷू߹‫ܕ‬ม਺͕ຬͨ͢ड़‫ޠ‬ͷू߹• Ϩίʔυ΍ϥϕϧू߹ͷഉ൓ੑ΍౳ՁੑΛड़‫͠ͱޠ‬ɼ୯ҰԽʹࣅͨॲཧͰड़‫߹ूޠ‬ͷ੍໿Λղফ• ΞϧΰϦζϜͷਖ਼౰ੑͷূ໌͢ΔͨΊʹϨίʔυͷଟॏू߹ʹΑΔҙຯ࿦Λఆ͍ٛͯ͠ΔͬΆ͍ߏ੒•എ‫ܠ‬•͓͞Β͍ɿLetଟ૬ͷ‫ܕ‬ਪ࿦
•[Ohori 1995]•[Osinski 2006]•·ͱΊ·ͱΊ• Ϩίʔυ‫ࢉܭ‬ͷ‫͚ͭܕ‬ɼͨͷ͍͠ʂ• [Ohori 1995]• SML# ͷ‫ܕ‬γεςϜͷ‫ૅج‬• ࿈઀Λαϙʔτ͠ͳ͍͔ΘΓʹޮ཰తʹ‫ܕ‬ਪ࿦͕ՄೳɼՃ͑ͯޮ཰తίʔυ΁ͱίϯύΠϧͰ͖Δ• Ϩίʔυ‫ࢉܭ‬ͷ͏ͪͰ͸ൺֱత‫͕ܕ‬Θ͔Γ΍͍͢ʁ• [Osinski 2006]• ‫ػ‬ೳ໘Ͱ͸ “ສೳ” Β͍͠ʢূ໌ະಡʣ
• ࣮૷͠ͳ͍͜ͱʹ͸ಈ࡞࣌ؒ΍࢖༻‫͕ײ‬Θ͔Βͳ͍ऄ଍• ࣮͸ਡ๚͕࣮૷ͨ͠

ͱ͍͏‫ʹޠݴ‬΋

[Ohori 1995] ͷ‫ܕ‬γεςϜ͕औΓࠐ·Ε͍ͯ·͢
https://github.com/gfngfn/Macrodown