Programming Computable Functions: Difference between revisions

Revision as of 08:49, 24 May 2022

Revision as of 21:05, 30 September 2022

Line 1:

{{Short description|A typed functional language}}

In [[computer science]], '''Programming Computable Functions''' (PCF) is a [[type system|typed]] [[Functional programming|functional language]] introduced by [[Gordon Plotkin]] in 1977,<ref name="Plotkin 1977" /> based on previous unpublished material by [[Dana Scott]].<ref {{r|group=note>|r="PCF is a programming language for computable functions, based on LCF, Scott’s logic of computable functions." {{harvr|name=Plotkin| 1977}}. ''Programming Computable Functions'' is used by {{harv|Mitchell|1996}}. It is also referred to as ''Programming with Computable Functions'' or ''Programming language for Computable Functions''.</ref>}} It can be considered to be an extended version of the [[typed lambda calculus]] or a simplified version of modern typed functional languages such as [[ML programming language|ML]] or [[Haskell (programming language)|Haskell]].

A [[fully abstract]] model for PCF was first given by [[Robin Milner|Milner]].<ref name="Milner (1977)." /> However, since Milner's model was essentially based on the syntax of PCF it was considered less than satisfactory.<ref (name="Ong, 1995)." /> The first two fully abstract models not employing syntax were formulated during the 1990s. These models are based on [[game semantics]]<ref (name="Hyland and2000" Ong, 2000;/><ref name="Abramsky, Jagadeesan,2000" and Malacaria, 2000)/> and [[Kripke logical relations]].<ref (name="O'Hearn and1995" Riecke, 1995)./> For a time it was felt that neither of these models was completely satisfactory, since they were not effectively presentable. However, [[Ralph Loader]] demonstrated that no effectively presentable fully abstract model could exist, since the question of program equivalence in the finitary fragment of PCF is not decidable.<ref name="Loader 2001" />

==Syntax==

Line 46:

** '''Y''' is interpreted by taking the [[least fixed point]] of the argument

This model is not fully abstract for PCF; but it is fully abstract for the language obtained by adding a ''[[parallel or]]'' operator to PCF (p.&nbsp;293 in the<ref name="Hyland and Ong 2000" reference below)./>{{rp|293}}

== Notes ==

Line 52:

== References ==

{{reflist|refs=

*{{ cite journal

<ref name="Plotkin 1977">{{cite journal

| first = Dana S.

| last = Scott

| authorlink = Dana Scott

| title = A type-theoretic alternative to CUCH, ISWIM, OWHY

| journal = Unpublished Manuscript

| url = https://www.cs.cmu.edu/~kw/scans/scott93tcs.pdf

| year = 1969

}} Appeared as {{cite journal | first = Dana S. | last = Scott | authorlink = Dana Scott | title = A type-theoretic alternative to CUCH, ISWIM, OWHY| journal = [[Theoretical Computer Science (journal)|Theoretical Computer Science]] | volume=121 | pages = 411&ndash;440 | year = 1993 | doi=10.1016/0304-3975(93)90095-b | doi-access = free }}

*{{ cite journal

| first = Gordon D.

| last = Plotkin

Line 74 ⟶ 66:

| url = http://homepages.inf.ed.ac.uk/gdp/publications/LCF.pdf

| doi-access = free

}}</ref>

*<ref name="Milner 1977">{{cite journal

| first = Robin

| last = Milner

Line 87 ⟶ 79:

| hdl = 20.500.11820/731c88c6-cdb1-4ea0-945e-f39d85de11f1

| hdl-access = free

}}</ref>

*<ref name="Ong 1995">{{cite book

|author first = JohnOng, C.-H. L.

|year last = Mitchell1995

|title = Handbook of Logic in Computer Science

| authorlink = John C. Mitchell

|chapter = Correspondence between Operational and Denotational Semantics: The Full Abstraction Problem for PCF

| title = Foundations for Programming Languages

|editor = Abramsky, S.

| year = 1996

|editor2 = Gabbay, D.

| isbn = 9780262133210

|editor3 = Maibau, T. S. E.

| chapter = The Language PCF

|pages = 269–356

| chapter-url = https://theory.stanford.edu/~jcm/books/fpl-chap2.ps

|publisher = Oxford University Press

}}

|chapter-url = http://users.comlab.ox.ac.uk/luke.ong/publications/index.html

*{{ cite journal

|access-date = 2006-01-19

|archive-url = https://web.archive.org/web/20060107195328/http://users.comlab.ox.ac.uk/luke.ong/publications/index.html#

|archive-date = 2006-01-07

|url-status = dead

}}</ref>

<ref name="Hyland 2000">{{cite journal

|author1=Hyland, J. M. E. |author2=Ong, C.-H. L.

|name-list-style=amp | title = On Full Abstraction for PCF

| journal = Information and Computation

| year= 2000

| pages = 285–408

| volume = 163

| issue = 2

| doi = 10.1006/inco.2000.2917|url=https://ora.ox.ac.uk/objects/uuid:63c54392-39f3-46f1-8a68-e6ff0ec90218

}}</ref>

<ref name="Abramsky 2000">{{cite journal

| author = Abramsky, S., Jagadeesan, R., and Malacaria, P.

| title = Full Abstraction for PCF

Line 107 ⟶ 115:

| issue = 2

| doi = 10.1006/inco.2000.2930| url = http://qmro.qmul.ac.uk/xmlui/handle/123456789/13604

}}</ref>

*<ref name="O'Hearn 1995">{{ cite journal

|author1=Hyland, J. M. E. |author2=Ong, C.-H. L.

|name-list-style=amp | title = On Full Abstraction for PCF

| journal = Information and Computation

| year= 2000

| pages = 285–408

| volume = 163

| issue = 2

| doi = 10.1006/inco.2000.2917|url=https://ora.ox.ac.uk/objects/uuid:63c54392-39f3-46f1-8a68-e6ff0ec90218

}}

*{{ cite journal

|author1=O'Hearn, P. W. |author2=Riecke, J. G

|name-list-style=amp | title = Kripke Logical Relations and PCF

| journal = Information and Computation

| year = 1995

Line 127 ⟶ 125:

| issue = 1

| doi = 10.1006/inco.1995.1103|url=https://surface.syr.edu/lcsmith_other/3

}}</ref>

*<ref name="Loader 2001">{{ cite journal

| author = Loader, R.

| title = Finitary PCF is not decidable

Line 137 ⟶ 135:

| issue = 1–2

| doi = 10.1016/S0304-3975(00)00194-8| doi-access = free

}}</ref>

}}

*{{ cite journal

| first = Dana S.

| last = Scott

| authorlink = Dana Scott

| title = A type-theoretic alternative to CUCH, ISWIM, OWHY

| journal = Unpublished Manuscript

| url = https://www.cs.cmu.edu/~kw/scans/scott93tcs.pdf

| year = 1969

}} Appeared as {{cite journal | first = Dana S. | last = Scott | authorlink = Dana Scott | title = A type-theoretic alternative to CUCH, ISWIM, OWHY| journal = [[Theoretical Computer Science (journal)|Theoretical Computer Science]] | volume=121 | pages = 411&ndash;440 | year = 1993 | doi=10.1016/0304-3975(93)90095-b | doi-access = free }}

*{{ cite journalbook

| first = John C.

| last = Mitchell

| authorlink = John C. Mitchell

| title = Foundations for Programming Languages

| year = 1996

| isbn = 9780262133210

| chapter = The Language PCF

| chapter-url = https://theory.stanford.edu/~jcm/books/fpl-chap2.ps

}}

*{{cite book

|author = Ong, C.-H. L.

|year = 1995

|title = Handbook of Logic in Computer Science

|chapter = Correspondence between Operational and Denotational Semantics: The Full Abstraction Problem for PCF

|editor = Abramsky, S.

|editor2 = Gabbay, D.

|editor3 = Maibau, T. S. E.

|pages = 269–356

|publisher = Oxford University Press

|chapter-url = http://users.comlab.ox.ac.uk/luke.ong/publications/index.html

|access-date = 2006-01-19

|archive-url = https://web.archive.org/web/20060107195328/http://users.comlab.ox.ac.uk/luke.ong/publications/index.html#

|archive-date = 2006-01-07

|url-status = dead

}}

==External links==