|
5. 嫄댁꽕�쟻 怨꾩궛踰� CC[2]
CC(Calculus of Constructions)�뒗 �쓽議댁쟻 ����엯�씠濡� �떆�뒪�뀥�쑝濡� ����왂 怨좎감 �끉由щ�� �솗�옣�븳 寃껋씠吏�留� 諛섎뱶�떆 �끉由щ쭔 �엳�뒗 寃껋�� �븘�땲�떎. CC�뒗 �뿬�윭 媛�吏�媛� �엳吏�留� 蹂� �끉臾몄뿉�꽌�뒗 �닚�닔 CC(LEGO�뿉�꽌�뒗 PCC�씪 �븳�떎.)留� �냼媛쒗븳�떎. PCC瑜� �룞�씪�븯吏�留� �뿬�윭 媛�吏� 諛⑺뼢�뿉�꽌 �냼媛쒗븷 �닔�룄 �엳寃좎��留� �뿬湲곗뿉�꽌�뒗 ����엯 �빀�꽦 諛� ����엯寃��궗�쓽 怨꾩궛媛��뒫�꽦�쓣 �젣�쇅�븯怨� 媛꾨떒�엳 �냼媛쒗븯怨좎옄 �븳�떎.
5.1 CC: �빆�쓽 援ъ“
�쓽議� ����엯�뿉�뒗 �빆�씠 �룷�븿�릺�뼱 �엳�쑝誘�濡� CC�뿉�꽌 �뜑 �씠�긽 �빆怨� ����엯�쓣 援щ텇�븯�뒗 寃껋씠 臾댁쓽誘명븯�떎.
5.1.1 醫낅쪟(sort)
�몢 媛쒖쓽 醫낅쪟媛� �엳�떎. 醫낅쪟瑜� s, t濡� �몴�떆�븳�떎.
s ::= Prop | Type
5.1.2 �빆(term)
�빆��� a, b, c, A, B, C, M, N�쑝濡� �몴�떆�븳�떎.
M ::= v 蹂��닔
| s 醫낅쪟
| [x:M]M �엺�떎 �빆
| {x:M}M PI
| MM �쓳�슜
{x:A}B�뒗 �쓽 LEGO�쓽 �몴�쁽�씠�떎. �뵲�씪�꽌 �떎�쓬�쓣 �쓽誘명븳�떎.
1) �씠嫄곕굹,
2) (B媛� x�뿉 �쓽議댄븯吏� �븡�쓣 �븣)�씠�떎.
5.2 CC: 臾몃㎘(context)�쓽 援ъ“
臾몃㎘��� �젅�씠釉붿씠 遺숈뼱 �엳�뒗 媛��젙�쓽 由ъ뒪�듃�씠�떎. 臾몃㎘��� �볥줈 �몴�떆�븳�떎.
�� ::= [] | ��, x:A
媛��젙�쓽 �젅�씠釉붾줈 x, y, z瑜� �궗�슜�븯吏�留� �씠�윴 �궗�빆��� 蹂꾨줈 以묒슂�븯吏� �븡�떎. 臾몃㎘
�뿉�꽌 �젅�씠釉� �뱾��� 紐⑤몢媛� �긽�씠�빐�빞 �븳�떎. �씠 �쟾�뿉�뒗 媛��젙 �씠 紐낆젣�씪怨� �뻽吏�留� �씠�젣�뒗 紐낆젣�씪怨좊쭔 �븷 �닔�뒗 �뾾�떎�뒗 �젏�뿉 �쑀�쓽�빐�빞 �븳�떎.5.3 CC: �뙋�떒(judgement)�쓽 援ъ“
�뙋�떒�쓽 援ъ“�뒗 �옄�뿰 異붾줎�쓽 洹멸쾬怨� 媛숇떎.
�뿬湲곗뿉�꽌 �볥뒗 臾몃㎘�씠怨� a, A���(�깮�왂)
|
[1]Henk Barendregt. Introduction to Generalized Type Systems. J. Functional Programming, 1(2):125-154, April 1991.
[2]Zhaohui Luo. An Extended Calculus of Constructions. PhD thesis, Department of Computer Science, University of Edinburgh, June 1990.
[3]Robert Pollack. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, Department of Computer Science, University of Edinburgh, 1994.
[4]Luis E. Sanchis. Recursive Functionals. North-Holland 1992.
|
인 쇄
바로가기
�젙由ъ쬆紐낆뿉�꽌 �닚�솚�븿�닔 �궗�슜.hwp
[Size :
59 Kbyte
]
장바구니
