WOLFRAM

Wolfram Language & System Documentation Center

fg or Application[f,g]

represents the formal application of f to g.

Details
Details and Options Details and Options
Examples  
Basic Examples  
Applications  
Properties & Relations  
Possible Issues  
Neat Examples  
See Also
Related Guides
History
Cite this Page

Application

fg or Application[f,g]

represents the formal application of f to g.

Details

Examples

open all close all

Basic Examples  (2)

Represent a combinatory term:

Wolfram Language code: CombinatorSCombinatorKCombinatorK

Apply the standard reduction rules of combinatory logic:

Wolfram Language code: CombinatorSCombinatorKCombinatorKX //. {CombinatorSx_y_z_ :> xz(yz), CombinatorKx_y_ :> x}

Applications  (1)

Prove an identity among combinators:

Wolfram Language code: thm = CombinatorS(CombinatorK(CombinatorSCombinatorI))(CombinatorS(CombinatorKCombinatorK)CombinatorI) == ;
Wolfram Language code: proof = FindEquationalProof[thm, "CombinatorAxioms"]

Properties & Relations  (3)

Convert from a formal application to an application in the Wolfram Language:

Wolfram Language code: CombinatorSCombinatorKCombinatorK //. f_g_ :> f@g

Alternatively, replace the operator:

Wolfram Language code: CombinatorSCombinatorKCombinatorK /. Application -> Construct

Convert from a Wolfram Language application to a formal application:

Wolfram Language code: CombinatorS[CombinatorI][CombinatorI][CombinatorS[CombinatorI][CombinatorI]] //. f_@g_ :> fg

Get the reduction rules for some notable combinators:

Wolfram Language code: crules = AxiomaticTheory["CombinatorAxioms", "RewriteRules"]

Apply the rules to combinatory terms:

Wolfram Language code: CombinatorS(CombinatorK(CombinatorSCombinatorI))(CombinatorS(CombinatorKCombinatorK)CombinatorI) //. crules

Possible Issues  (1)

Many interesting combinatory terms do not have a normal form, so they keep changing forever:

Wolfram Language code: CombinatorSCombinatorICombinatorI(CombinatorSCombinatorICombinatorI) //. AxiomaticTheory["CombinatorAxioms", "RewriteRules"]

This term leads to a cycle of length 2:

Wolfram Language code: NestList[ReplaceAll[AxiomaticTheory["CombinatorAxioms", "RewriteRules"]], CombinatorSCombinatorICombinatorI(CombinatorSCombinatorICombinatorI), 4]//Column

Neat Examples  (2)

The reduction rule for the Turing combinator:

Wolfram Language code: TuringUAxioms = { ForAll[{x, y}, Uxy == y(xxy)] }

Prove that is a fixed-point combinator:

Wolfram Language code: FindEquationalProof[UU == (UU), TuringUAxioms]

Eliminate variables to convert arbitrary terms into combinator form:

Wolfram Language code: toCombinator[{v_}, v_] := CombinatorI; toCombinator[{v_}, e_] /; FreeQ[e, v] := CombinatorKe toCombinator[{v_}, e_v_] /; FreeQ[e, v] := e toCombinator[{v_}, x_y_] := CombinatorStoCombinator[{v}, x]toCombinator[{v}, y] toCombinator[{r__, v_}, e_] := toCombinator[{r}, toCombinator[{v}, e]]

Find the combinator that doubles its argument:

Wolfram Language code: toCombinator[{x}, xx]

Find the combinator for a function application:

Wolfram Language code: toCombinator[{f, g, x}, f(gx)]

Verify the result by applying the standard combinatory reductions for TemplateBox[{}, CombinatorS] and TemplateBox[{}, CombinatorK]:

Wolfram Language code: FixedPointList[ReplaceAll[AxiomaticTheory["CombinatorAxioms", "RewriteRules"]], CombinatorS(CombinatorKCombinatorS)CombinatorKfgx]//Column
Wolfram Research (2020), Application, Wolfram Language function, https://reference.wolfram.com/language/ref/Application.html.

Text

Wolfram Research (2020), Application, Wolfram Language function, https://reference.wolfram.com/language/ref/Application.html.

CMS

Wolfram Language. 2020. "Application." Wolfram Language & System Documentation Center. Wolfram Research. https://reference.wolfram.com/language/ref/Application.html.

APA

Wolfram Language. (2020). Application. Wolfram Language & System Documentation Center. Retrieved from https://reference.wolfram.com/language/ref/Application.html

BibTeX

@misc{reference.wolfram_2026_application, author="Wolfram Research", title="{Application}", year="2020", howpublished="\url{https://reference.wolfram.com/language/ref/Application.html}", note=[Accessed: 12-June-2026]}

BibLaTeX

@online{reference.wolfram_2026_application, organization={Wolfram Research}, title={Application}, year={2020}, url={https://reference.wolfram.com/language/ref/Application.html}, note=[Accessed: 12-June-2026]}