TypeScriptから構造体を奪って、関数だけでまた構造体を得るまでの道のり (チャーチ・エンコーディング)

これは定理証明支援系 Advent Calendar 2023の参加記事です。 なお、この記事はさほど定理証明は直接的には関係ありませんが、「周辺の分野」ということで寄稿させていただきました。 概要 この記事はラムダ計算などで登場する概念を、もっと身近な言語で説明してみよう、という試みのうちのひとつです。最初はチャーチ・エンコーディングの "気持ち" の部分をとりあえず理解するための記事を作ってみました。 (この他にもシリーズを展開していきたいなと思っています) 対象読者 関数だけでどこまでできるか、関数の限界を知りたい人 ラムダ計算・TaPLをこれから勉強したい人 チャーチ数・チャーチエンコーディングを勉強したものの、その "気持ち" を知りたい・納得したい人 白紙からチャーチ数・チャーチブール等の定義を構成できるようになりたい人 チャーチ数 (チャーチ・エンコーディング) のちょっと変