Une nouvelle C\(\beta\)-réduction dans la logique combinatoire (Q762137): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/0304-3975(84)90132-4 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2020478268 / rank | |||
Normal rank |
Revision as of 21:18, 19 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Une nouvelle C\(\beta\)-réduction dans la logique combinatoire |
scientific article |
Statements
Une nouvelle C\(\beta\)-réduction dans la logique combinatoire (English)
0 references
1984
0 references
In this paper we give a new reduction in combinatory logic analogous to \(\lambda\) \(\beta\)-reduction. Such problem has been studied by Curry, Hindley and Seldin. Curry's reduction based on abstraction algorithm \((abc_{\beta}f_{\beta})\) does not solve the problem completely. Hindley in his unpublished notes gives a new definition of equivalence between CL-reduction and \(\lambda\) \(\beta\)-reduction. The CL-reduction that we give is based on Hindley's characterisation of \(C\beta\)-reduction described in his later work. It consists of finding an abstraction algorithm [ ]\({}^ 0\) and a reduction in combinatory logic \(\succ^ 0\) satisfying certain properties. We define [ ]\({}^ 0\) and \(\succ^ 0\) and prove the theorem that the couple ([ ]\({}^ 0,\succ^ 0)\) has these properties.
0 references
lambda-beta-reduction
0 references
combinatory logic
0 references
abstraction algorithm
0 references
equivalence
0 references
CL-reduction
0 references