Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
Programming Computable Functions
open-in-new
<h2 id="syntax">Syntax</h2> <p>The <i>types</i> of PCF are inductively defined as </p> <ul><li>nat is a type</li> <li>For types <i>σ</i> and <i>τ</i>, there is a type <i>σ</i> → <i>τ</i></li></ul> <p>A <i>context</i> is a list of pairs <i>x : σ</i>, where <i>x</i> is a variable name and <i>σ</i> is a type, such that no variable name is duplicated. One then defines typing judgments of terms-in-context in the usual way for the following syntactical constructs: </p> <ul><li>Variables (if <i>x : σ</i> is part of a context <i>Γ</i>, then <i>Γ</i> ⊢ <i>x</i> : <i>σ</i>)</li> <li>Application (of a term of type <i>σ</i> → <i>τ</i> to a term of type <i>σ</i>)</li> <li><a href="/facts/%CE%9B-abstraction/DaD3RuQ4">λ-abstraction</a></li> <li>The <a href="/facts/Fixed-point_combinator/mRqKblYz">Y</a> fixed point combinator (making terms of type <i>σ</i> out of terms of type <i>σ</i> → <i>σ</i>)</li> <li>The successor (succ) and predecessor (pred) operations on nat and the constant 0</li> <li>The conditional if with the typing rule:</li></ul> Γ ⊢ t : nat , Γ ⊢ s 0 : σ , Γ ⊢ s 1 : σ Γ ⊢ if ( t , s 0 , s 1 ) : σ {\displaystyle {\frac {\Gamma \;\vdash \;t\;:{\textbf {nat}},\quad \quad \Gamma \;\vdash \;s_{0}\;:\sigma ,\quad \quad \Gamma \;\vdash \;s_{1}\;:\sigma }{\Gamma \;\vdash \;{\textbf {if}}(t,s_{0},s_{1})\;:\sigma }}} (nats will be interpreted as booleans here with a convention like zero denoting truth, and any other number denoting falsity) <h2 id="semantics">Semantics</h2> <h3>Denotational semantics</h3> <p>A relatively straightforward semantics for the language is the Scott model. In this model, </p> <ul><li>Types are interpreted as certain <a href="/facts/Domain_theory/G1wRMK2K">domains</a>. <ul><li> [ [ nat ] ] := N ⊥ {\displaystyle [\![{\textbf {nat}}]\!]:=\mathbb {N} _{\bot }} (the natural numbers with a bottom element adjoined, with the flat ordering)</li> <li> [ [ σ → τ ] ] {\displaystyle [\![\sigma \to \tau \,]\!]} is interpreted as the domain of <a href="/facts/Scott-continuous/7CqoURj0">Scott-continuous</a> functions from [ [ σ ] ] {\displaystyle [\![\sigma ]\!]\,} to [ [ τ ] ] {\displaystyle [\![\tau ]\!]\,} , with the pointwise ordering.</li></ul></li> <li>A context x 1 : σ 1 , … , x n : σ n {\displaystyle x_{1}:\sigma _{1},\;\dots ,\;x_{n}:\sigma _{n}} is interpreted as the product [ [ σ 1 ] ] × … × [ [ σ n ] ] {\displaystyle [\![\sigma _{1}]\!]\times \;\dots \;\times [\![\sigma _{n}]\!]} </li> <li>Terms in context Γ ⊢ x : σ {\displaystyle \Gamma \;\vdash \;x\;:\;\sigma } are interpreted as continuous functions [ [ Γ ] ] → [ [ σ ] ] {\displaystyle [\![\Gamma ]\!]\;\to \;[\![\sigma ]\!]} <ul><li>Variable terms are interpreted as projections</li> <li>Lambda abstraction and application are interpreted by making use of the <a href="/facts/Cartesian_closed/mPXAQps2">cartesian closed</a> structure of the category of domains and continuous functions</li> <li>Y is interpreted by taking the <a href="/facts/Least_fixed_point/JbcBLqTN">least fixed point</a> of the argument</li></ul></li></ul> <p>This model is not fully abstract for PCF; but it is fully abstract for the language obtained by adding a <i><a href="/facts/Parallel_or/jbI2EGlM">parallel or</a></i> operator to PCF.<a class="footnote-ref" id="fnref:9" href="#fn:9"><sup>9</sup></a>: 293 </p> <h2 id="notes">Notes</h2> <ul><li><a href="/facts/Dana_Scott/XEVddlVg">Scott, Dana S.</a> (1969). <a href="https://www.cs.cmu.edu/~kw/scans/scott93tcs.pdf">"A type-theoretic alternative to CUCH, ISWIM, OWHY"</a> (PDF). <i>Unpublished Manuscript</i>. Appeared as <a href="/facts/Dana_Scott/XEVddlVg">Scott, Dana S.</a> (1993). <a href="https://doi.org/10.1016%2F0304-3975%2893%2990095-b">"A type-theoretic alternative to CUCH, ISWIM, OWHY"</a>. <i><a href="/facts/Theoretical_Computer_Science_(journal)/Apbc0PDL">Theoretical Computer Science</a></i>. 121: 411–440. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2F0304-3975%2893%2990095-b">10.1016/0304-3975(93)90095-b</a>.</li> <li><a href="/facts/John_C._Mitchell/8tzw9FNg">Mitchell, John C.</a> (1996). <a href="https://theory.stanford.edu/~jcm/books/fpl-chap2.ps">"The Language PCF"</a>. <i>Foundations for Programming Languages</i>. MIT Press. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 9780262133210.</li></ul> <h2 id="external-links">External links</h2> <ul><li><a href="http://www.cs.bham.ac.uk/~mhe/papers/RNC3.pdf">Introduction to RealPCF</a></li> <li><a href="https://web.archive.org/web/20071213234103/http://www.cs.pomona.edu/classes/cs131/Parsers/parsePCF.sml">Lexer and Parser for PCF written in SML</a></li></ul> <h2 id="references">References</h2> <ol> <li id="fn:1"><p>Plotkin, Gordon D. (1977). "LCF considered as a programming language" (PDF). Theoretical Computer Science. 5 (3): 223–255. doi:10.1016/0304-3975(77)90044-5. <a href="/wiki/Gordon_Plotkin" target="_blank">/wiki/Gordon_Plotkin</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li> <li id="fn:2"><p>"PCF is a programming language for computable functions, based on LCF, Scott’s logic of computable functions."[1] Programming Computable Functions is used by (Mitchell 1996). It is also referred to as Programming with Computable Functions or Programming language for Computable Functions. <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li> <li id="fn:3"><p>Milner, Robin (1977). "Fully abstract models of typed λ-calculi" (PDF). Theoretical Computer Science. 4: 1–22. doi:10.1016/0304-3975(77)90053-6. hdl:20.500.11820/731c88c6-cdb1-4ea0-945e-f39d85de11f1. <a href="/wiki/Robin_Milner" target="_blank">/wiki/Robin_Milner</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li> <li id="fn:4"><p>Ong, C.-H. L. (1995). "Correspondence between Operational and Denotational Semantics: The Full Abstraction Problem for PCF". In Abramsky, S.; Gabbay, D.; Maibau, T. S. E. (eds.). Handbook of Logic in Computer Science. Oxford University Press. pp. 269–356. Archived from the original on 2006-01-07. Retrieved 2006-01-19. <a href="https://web.archive.org/web/20060107195328/http://users.comlab.ox.ac.uk/luke.ong/publications/index.html" target="_blank">https://web.archive.org/web/20060107195328/http://users.comlab.ox.ac.uk/luke.ong/publications/index.html</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></p></li> <li id="fn:5"><p>Hyland, J. M. E. & Ong, C.-H. L. (2000). "On Full Abstraction for PCF". Information and Computation. 163 (2): 285–408. doi:10.1006/inco.2000.2917. <a href="https://ora.ox.ac.uk/objects/uuid:63c54392-39f3-46f1-8a68-e6ff0ec90218" target="_blank">https://ora.ox.ac.uk/objects/uuid:63c54392-39f3-46f1-8a68-e6ff0ec90218</a> <a href="#fnref:5" class="footnote-back-ref">↩</a></p></li> <li id="fn:6"><p>Abramsky, S., Jagadeesan, R., and Malacaria, P. (2000). "Full Abstraction for PCF". Information and Computation. 163 (2): 409–470. doi:10.1006/inco.2000.2930.{{cite journal}}: CS1 maint: multiple names: authors list (link) <a href="http://qmro.qmul.ac.uk/xmlui/handle/123456789/13604" target="_blank">http://qmro.qmul.ac.uk/xmlui/handle/123456789/13604</a> <a href="#fnref:6" class="footnote-back-ref">↩</a></p></li> <li id="fn:7"><p>O'Hearn, P. W. & Riecke, J. G (1995). "Kripke Logical Relations and PCF". Information and Computation. 120 (1): 107–116. doi:10.1006/inco.1995.1103. <a href="https://surface.syr.edu/lcsmith_other/3" target="_blank">https://surface.syr.edu/lcsmith_other/3</a> <a href="#fnref:7" class="footnote-back-ref">↩</a></p></li> <li id="fn:8"><p>Loader, R. (2001). "Finitary PCF is not decidable". Theoretical Computer Science. 266 (1–2): 341–364. doi:10.1016/S0304-3975(00)00194-8. <a href="https://doi.org/10.1016%2FS0304-3975%2800%2900194-8" target="_blank">https://doi.org/10.1016%2FS0304-3975%2800%2900194-8</a> <a href="#fnref:8" class="footnote-back-ref">↩</a></p></li> <li id="fn:9"><p>Hyland, J. M. E. & Ong, C.-H. L. (2000). "On Full Abstraction for PCF". Information and Computation. 163 (2): 285–408. doi:10.1006/inco.2000.2917. <a href="https://ora.ox.ac.uk/objects/uuid:63c54392-39f3-46f1-8a68-e6ff0ec90218" target="_blank">https://ora.ox.ac.uk/objects/uuid:63c54392-39f3-46f1-8a68-e6ff0ec90218</a> <a href="#fnref:9" class="footnote-back-ref">↩</a></p></li> </ol>