WOLFRAM

Wolfram言語 ＆ システムドキュメントセンター

fg または Application[f,g]

f の g への形式的な適用を表す．

詳細
Details and Options Details and Options
例題  
例  
アプリケーション  
特性と関係  
考えられる問題  
おもしろい例題  
関連項目
関連するガイド
履歴
引用書式

Application

fg または Application[f,g]

f の g への形式的な適用を表す．

詳細

  • Applicationは二項演算子である．fgh はApplication[Application[f,g],h]と解釈される．
  • Application[f,g]は組込みの意味を持たない．
  • Application[f,g]は fg と入力できる．記号 は ap または \[Application]と入力する．
  • Applicationを使ってコンビネータを含む項が構築できる．

例題

すべて開く すべて閉じる

例  (2)

結合項を表す：

Wolfram Language code: CombinatorSCombinatorKCombinatorK

コンビネータ論理の標準的な削減規則を適用する：

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

アプリケーション  (1)

コンビネータ内の恒等式を証明する：

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

特性と関係  (3)

形式的な適用からWolfram言語における適用に変換する：

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

演算子を置き換えることもできる：

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

Wolfram言語における適用から形式的な適用に変換する：

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

著名なコンビネータについての削減規則を得る：

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

結合項に規則を適用する：

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

考えられる問題  (1)

興味深い結合項の多くは，通常の形を持たず，永遠に変り続ける：

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

この項は長さ2の循環になる：

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

おもしろい例題  (2)

チューリング(Turing)の コンビネータの削減規則：

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

は固定点のコンビネータであることを証明する：

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

変数を除いて任意の項をコンビネータ形式に変換する：

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]]

引数を2倍にするコンビネータを求める：

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

関数適用のためのコンビネータを求める：

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

TemplateBox[{}, CombinatorS]とTemplateBox[{}, CombinatorK]についての標準結合削減規則を適用して結果を検証する：

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

テキスト

Wolfram Research (2020), Application, Wolfram言語関数， 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: 15-September-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: 15-September-2026]}