著者

布川 博士 富樫 敦 野口 正一

雑誌

全国大会講演論文集

巻号頁・発行日

vol.33, pp.7-8, 1986-10-01

---

The semantics of Backus FP is given by the it's formal system FFP. i.e. f:x=y is defined by using FFP's meaning function μ if and only if μ(fFFP, xFFP) reduce to yFFP (where subscript FFP indicates the version of an FP object translated into an FFP one). When recursively defined function is computed, in Lisp 1.5 of use the external mechanism LABEL notation, in Curry's system of the lambda or combinatory calculus, the fixed point operater 'Y is used. Backus[Backus 78] used for this purpose the meta composition rule in μ and succeeded in solving recursive equations according to the reductuion system FFP having meta composition reduction rule without any external mechanism or Y. Williams showed the formal rules for translation of FP into FFP representation which preserve meaning of FP functions. By his algorithm Πf, f=Ef in FP is translated into F=<Πf(Ef)>, for example fact=eq0→-1 ; ×○[id fact○sub1]≡Efact, is tanslated into FACT≡Πfact(Efact)=EQ○2→1 ; ×○[ID○2 APPLY○[1 SUB 1○2]] Then according to the reduction rule of μ, μ(<FACT>,3) is reduced to the most simple expression 6 as follows μ(<FACT>,3)⇒#μ(FACT, <<FACT>,3>)⇒*6 The first reduction is an application of meta composition rule. To be precise, we should write e. g. EQ0○2 as <COMP EQ0 2> but to save space we used an abbreviation which is similar to the FP notation. In this representation algorithm, similar to the ccase of Y usage, the recursively defined function f=Ef in FP is translated into fFFP dose not contain function variable f. In this paper we propose a type assignment system for recursive functions in FP by assigning the type to the corresponding FFP representation aloging these lines.