Japanese Translation:

著者は、有限関数型プログラミング、関係論的プログラミング（Datalog/SQL）、およびテンソル代数を組み合わせた新規のハイブリッドシステムλFSを提示しました。λFSでは、関係を有限サポートを持つ関数として扱い、データ構造（ハッシュテーブルやバランスドツリーなど）を用いて実行時に明示的に表現し、デフォルト値を用いて任意の共域に一般化しています。

重要な革新点は、データベースの哲学（実行速度の優先）とプログラミング言語の哲学（終了に関する厳密な推論の要求）、特に循環クエリにおける両者の緊張関係を解決することにあります。再帰は非終止リスクや評価順序依存性により依然として大きな課題ですが、システムでは左から右へとの評価に単純なコストモデルを用いる戦略、成果を「はい/いいえ/わからない」として境界化する非決定論的な評価順序、および Plotkin の LCF 作業に触発された並列かつの演算子を導入して決定的性を回復させるなどの戦略を検討しています。miniKanren や Andorra Prolog などの先例を取り入れ、システムの性能責任とプログラマの性能責任をバランスさせる効率的な評価戦略の策定を目指しています。将来の作業では、これらのアプローチを実装し、循環クエリに対する強力な最適化（例えば三角形検出）を可能にするとともに、直感的な正当性と堅牢な性能を確保することを目指します。

有限型関数プログラミング（λFS）の非終端性と評価順序：2026 年 6 月の講演より

2026 年 6 月、私は FLOPS で**有限型関数プログラミング（λFS）**に関する講演を行いました。これには、関係論的プログラミング（Datalog, SQL）、テンソル代数など、これまでの試みである Datafun を含む最新のアプローチが統合されています。

以下に λFS の基本定義、再帰処理における課題、およびそれへの 3 つの解決案を整理します。

1. λFS の基本概念とデータ構造

λFS では、**関係（Relation）**を関数として扱います。

関数の定義

関係 $R$ を関数 $R(x)$ と見なします。
真偽判定:
- $x$ が $R$ に含まれる $\Rightarrow R(x) = \text{true}$
- $x$ が $R$ に含まれない $\Rightarrow R(x) = \text{false}$

有限性 (Finiteness) と支持 (Support)

有限性の保証: $R(x) = \text{true}$ となる入力 $x$ は有限個しか存在しません。この入力の集合を**「支持（support）」**と呼びます。
型システム: 論文では、この関数が有限な支持を持つことを保証するための型システムを導入しています。

データ表現 (実行者)

実行時には、有限な真偽関数を以下のデータ構造で表します：
- ハッシュテーブル
- バランスド・ツリー（例：AVL ツリー）
- これらの集合が**「表」**として機能します。

値の拡張とマップとしての一般化

この概念は二値に限定されず、任意の共域を持ちつつ「デフォルト値」を定義できるものへ拡張可能です。
- デフォルト値例：
```
false
```
  （ブール型）,
```
0
```
  （整数型）など。
有限関数としての定義:
- 「キーと値を持つテーブル」として表現されます。
- 表のキーが支持に属しない場合 $\Rightarrow$ 暗黙的にデフォルト値にマッピングされます。
テンソル代数との関係:
- テンソル代数も、本質的には非ブール型（実数値など）の有限マップにおける関係演算アルゴリズムとして捉えることができます。

2. 無限ループと評価順序の問題点

講演では再帰処理が今後の課題であるという点に触れました。**「なぜ難しいのか？」**という問いに対し、以下の二つの主な困難が指摘されます。

非終端性（無限ループ）

再帰によって無限ループが発生し得ます。
通常、これに対処するにはドメイン理論を用いますが、近年は流行を失っており、深掘りには畏怖の対象となっています。¹

評価順序（Evaluation Order）の重要性

非終端性や副作用が絡むと、プログラムが終了するか否かが決定的に変わります。
ラムダ計算における差異:
- ```
Call-by-name
```
  （名前による呼び出し）: 再帰呼び出しを繰り返す。
- ```
Call-by-value
```
  （値による呼び出し）: 引数を実際に評価してから呼び出す。
- これらの違いにより、終了するかどうかの挙動が分かれます。
関係言語における広義性: 関係言語では、「評価順序」はより広範な意味を持ちます。

具体的な問題例：クエリの実行順序

以下の定義で構成されるクエリ $Q$ を考えます：

R, S : nat => bool    (有限関数、テーブルとして表現)
test : nat -> bool    (ブラックボックス predicate)
Q(x) := R(x) and test(x) and S(x)   (クエリ)

```
=>
```
: テーブルとして表現される有限関数。
```
->
```
: 手続きやクロージャとして表現される任意の関数。

シナリオ A：コストの低いテストを優先（順次処理）

test(x)

はコストが高いが、テーブルルックアップは安価です。したがって、先に高速なルックアップを行い、後で高コストなテストを行う方が効率的です。

# 効率の良い順序
[x for x in R if x in S if test(x)]

シナリオ B：データ量の差を活かす

が非常に小さい場合、小集合を反復処理することで大幅な時間節約を図れます。

# より効率的な順序（小集合 S をループ主体）
[x for x in S if x in R if test(x)]

シナリオ C：評価順序による「終了性」の分岐（重要）

もし

test

が特定の値で無限ループする場合、評価順序がクエリの結果（終了するか否か）を決定づけます。

設定例:

$R := {\text{"hello"}, \text{"world"}}$
$S := {\text{"hello"}, \text{"alice"}}$
$\text{test}(x) := (x == \text{"hello"}) \lor \text{loop-forever()}$

結果の比較:

左から右の評価（順序 A/C の組み合わせ等）
- まず $\text{test}(\text{"hello"})$ を呼び出し成功。
- 次に $\text{test}(\text{"world"})$ を呼び出す $\Rightarrow$ 無限ループに陥る。
- 結果: 異常終了。
共通部分からテストへ（順序 B）
- まず $R \cap S = {\text{"hello"}}$ のみを抽出する。
- 次に $\text{test}(\text{"hello"})$ を呼ぶだけ。
- 結果: 正常終了。

根本的なジレンマ

この問題は λFS だけでなく、ユーザー定義関数をサポートする SQL や Datalog エンジン全体に共通します。データベースの前提とプログラミング言語の前提との間に緊張関係が存在します：

DB 側の視点: クエリエンジンが実行戦略を選択し、パフォーマンスを最適化する（実装詳細）。
PL 側の視点: プログラムの振る舞い（終了性など）を構成論的に推論できる必要がある。

λFS は両者の世界を橋渡ししようとしましたが、どちらかの視点を優先するか、あるいは非常に細かな調整を行うというジレンマに直面しています。

3. 提案するセマンティクスの方向性（案）

再帰や非終端性をサポートしつつ、λFS でどのように処理すべきかについて、以下の 3 つの方向性を挙げてみます。

案 1：左から右の評価（単純なコストモデル）

最も直感的で自然なアプローチです。典型的なプログラミング言語のアプローチであり、クエリプランニングを行わず、実行責任を完全にプログラマに委ねます（Rob Simmons 氏も推奨）。²

メリット

コストの予測可能性: クエリの実行時間を推論しやすく、「弾丸を食べる」姿勢によりプログラマのパフォーマンス責任が明確化されます。
型システムとの整合性: この戦略は、有限関数プログラミングにおける型システムと完全に一致します。当初は弱点だと思っていましたが、理にかなった設計であることが分かりました。

実装のメカニズム

結合（conjunction）$n$ は最大 $n$ つのネストされたループに分解されます。

一般の場合:

for x in R:
    for y in S:
        yield (x,y)

変数が既に関連付けられている場合（Grounded）:

for x in R:
    if x not in S: continue  # テスト処理
    yield x

制限事項

予測可能なパフォーマンスが得られない場合があります。
代表的な例: 三角形のクエリ
```
edge(x,y) and edge(y,z) and edge(x,z)
```
は、左から右の評価では二次的なコストをかけて線形の結果を得てしまい、最適化できません。³

案 2：非決定論的評価順序による宣言的最適化

評価順序を「未指定」とし、クエリプランナーに自由度を与えます（典型的なデータベースの手法）。

動作原理

実行集: $\text{test}$ は $R \cup S$ の内の値に対してのみ呼び出され、少なくとも $R \cap S$ の中の値については必ず呼ばれます。
終了性の拡張: 「Yes/No」から「Yes/No/Maybe」へと拡張されます。
- $\text{test}$ が $R \cup S$ 内ですべて収束すればクエリは終了。
- $R \cap S$ 内で一部の値で発散すればクエリが発散。

セマンティクス設計の難点

操作論的アプローチ: ボトムアップの論理プログラミングセマンティクスを定義し、評価順序の違いを捉える方法が見出せていません。λFS の有限関数をどのように eagerly（積極的）に評価すべきかも課題です。⁴
意味論的アプローチ: ドメイン理論と非決定論性の拡張を加味する方向性は自然ですが、パワー・ドメイン等の理論習熟度不足により実現が困難です。

案 3：「並列かつ (parallel and)」による最も宣言的な振る舞い

test(x)

が発散してもクエリ全体が発散しないように、より並列的に振る舞うことを目指します。これは Gordon Plotkin の**「並列 OR」**³に由来する命名です。⁵

従来の

and

(順次型) の問題点

左側を先に評価し、偽 (
```
false
```
) が返れば短路（short-circuit）しますが、論理的結合は対称であるべきであり、左偏しています。
- $\bot \land x = \bot$ （$x$ の評価に至らない）

「並列かつ」の定義

両方の側が対称性と**連続性（continuity）**を維持するように修正します。⁶

式	結果	特徴
`false and x`	`false`	短路；$x$ は評価されない
`true and x`	`x`	通常処理
`x and false`	`false`	$x$ の追加評価は不要（対称性）
`x and true`	`x`	$x$ を保持

エフェクト：発散の回避

左から右の評価では

test("world")

が無限ループしましたが、並列かつでは：

$R(\text{"world"}) \land \text{test}(\text{"world"})$ は、片方が $\bot$（または false）だと直ちに $\bot$ と扱われます。
結果として、処理順序が変わっても $Q = {\text{"hello"}}$ という直感的に正しい結果が得られます。

実装の可能性と課題

ミニカンレン (miniKanren) の検索戦略や、Andorra Prolog のアプローチがヒントとなります。
「公平な結合（fair conjunction）」を実装し、最悪ケースでの最適化 joins を iterator インターフェースを用いて実現することは可能だと推測します。⁷

結論

λFS はデータベースとプログラミング言語の二つの世界を架け橋とする試みですが、評価順序や終了性の問題は依然として未解決です。

案 1はシンプルで予測可能だが、特定のパターン（循環クエリ）で性能が劣化する。
案 2と案 3は宣言的な最適化を目指すが、理論的・実装上の難易度が高い。

これらの課題に対する妥当な解決策についてご意見や共創をご希望の場合は、以下のアドレスへご連絡ください（PGP/暗号化通信推奨）。

連絡先: qnrxunery@tznvy.pbz (rot13 化済み)

脚注

再帰の二重性:
- (a) ラズビー（遅延評価）で計算される**「再帰関数」**（体は適用時まで評価されない）。
- (b) λFS の有限関数である**「再帰関係」**（ボトムアップ型で eagerly 計算される）。
- 後者は前者で定義可能であり、再帰は反復（iteration）を定義するのに十分です。↩
三角形クエリの非効率性:
- ```
edge = {(1, x) : x ∈ [1..n]} ∪ {(x, 1) : x ∈ [1..n]}
```
  を設定すると、三角形の答えは $\Theta(n)$ 個ありますが、前置部分に満たすトリプルは $\Theta(n^2)$ 個あります。左から右の評価では二次的なコストをかけて線形の結果を得てしまいます。↩
並列 OR の起源:
- Gordon Plotkin の LCF Considered as a Programming Language (1977) に起源があると信じていますが、入門書としては講義ノート（p64, §8.1 "Failure of full abstraction"）が分かりやすいです。↩
公平な結合:
- miniKanren の検索戦略や Will Byrd 氏の研究（Andorra Prolog における並列的 conjunction）から解決の糸口が見つかる可能性があります。⁴
Meven Lennon-Bertrand 氏の議論:
- Mastodon で行われた議論でも、ブール値における並列 OR/AND と公平な論理プログラミングの結合の有効性が問題視されており、妥当であると考えられています。↩

クエリ言語における評価順序と非終止