Amosapientiam

備忘録

F*(F Star)の複雑な型システムの何が嬉しいのか?

マイクロソフトが開発中のF* という依存型プログラミング言語を少し触ってみました。 この言語には強力で複雑な型システムが組み込まれています。 現状、依存型言語は世間にはあまり広まっていませんので

  • F*とは?
  • 複雑な型ってなんだろう?
  • 複雑な型システムを組み込んで何が嬉しいんだろう?
  • 何が嬉しくないんだろう?

と疑問をお持ちになる方も多いだろうと思います。 この記事ではF*で使われている複雑な型の一部と、複雑な型を持つことの利点・欠点の一部を述べ、それを簡単なコード例を通じて体感してみます。

疑問に対する答え

F*とは?

マイクロソフトと Inria が開発中のプログラミング言語です。 依存型や monadic effect などが組み込まれており、複雑な仕様が型で表現できます。構文は OCaml や F#などのML系関数型言語に似ています。 詳しくは下記のリンクたちを参照。

F*の複雑な型システムって?

上の説明から、 F*の型システムには依存型と effectが組み込まれていることがわかります。

依存型

型の中に値が現れる型です。

依存型 - Wikipedia

例えば、 「整数型で100より大きい値」の型「文字列で、長さが10より小さい値」の型などです。

effect

F* では、関数型には

  • 純粋で必ず停止する関数である
  • 停止するとは限らない
  • 副作用があるかもしれない
  • ...

などの情報が埋め込まれています。

型が複雑であることの利点

型は仕様でもあること、型検査は仕様検証でもあることは以前の記事で書きました。 この観点から、複雑で表現力の高い型を持つことには以下の利点があると言えます。

  • 型によって複雑な仕様が表現でき、実装が複雑な仕様を満たすことを型検査によって保証できる。

型が複雑であることの欠点

型が複雑になるにつれ、コンパイラが自力で型検査ををするのは難しくなります。コンパイラの助けになるように人間が自力で型付けのヒントを書かなければならない場面も増えます。極端な場合は複雑な証明をひたすら書くハメになります。 *1

F*コードの例

以上で挙げた特徴がどういうものなのか、具体的にシンプルな関数を例にとって確認してみます。

今回の関数

以下の関数を例にとります。

// 仕様:関数gcdは2つの正整数を受け取り、その(最大)公約数を返す
let rec gcd a b =
    match compare_int a b with
    | Gt -> gcd (a - b) b
    | Lt -> gcd b a
    | Eq -> a

この関数は少なくともコンパイルが通ります。

"match with" は場合分けの構文です。a と b の2つの引数を受け取り、a と b を大小比較し、

  • a の方が大きかった場合(greater than)は gcd (a-b) b を返り値とし、
  • a の方が小さかった場合(less than)は gcd b a を返り値とし、
  • a と b が等しい場合(equal)は a を返します。

確認したい性質・仕様

私は関数gcdを「正整数 2 つの最大公約数を返す関数」のつもりで書いたのですが、本当に正しく書けているでしょうか?それをコンパイラ(の中の型検査器)に保証してもらうためには、gcd に「正整数を2つ受け取り、その最大公約数を返す関数」の型が付くことを確認してもらえばよいです。

この記事では簡単のため、もう少し弱い仕様である「関数 gcd は正整数を2つ受け取り、その公約数を返す」ことの確認を最終目標とし、そのために gcd に「生成数を2つ受け取り、その公約数を返す関数」の型を付けるところまでを目指します。

いきなり複雑な型を読み解くのは難しいので、最初は弱い簡単な型を付けて、徐々に強くしていく方針で説明します。

返り値が整数であることを保証する型

少なくとも gcd には 整数を2つ受け取って整数を返す関数であってほしいです。 これを表す型は F*ではint -> int -> ML intです。

"ML"というのはこの関数が純粋で total だとは限らないという断り書きです。 返り値の型の前に ML と書くことで、「この関数は参照透過でないかもしれないし、クラッシュするかもしれないし、ひょっとしたら停止しないかもしれないが、停止した時には必ず int 型の値を返す」という意味の型になります。 よくあるプログラミング言語の関数の型の意味と同じです。

gcdが int ->int -> ML intの型を持つかどうかF*コンパイラにチェックしてもらいます。

val gcd : int -> int -> ML int
let rec gcd a b =
    match compare_int a b with
    | Gt -> gcd (a-b) b
    | Lt -> gcd b a
    | Eq -> a

上のコードは無事型検査が通ります。 gcdの実装が「整数を2つ受け取って(停止すれば)整数を返す関数」であることは保証されました。

停止性・参照透過性などまで保証する型

"ML"の代わりに"Tot"と書く場合、F*では「関数は副作用を持たず、必ず停止し、int 型の値を返す関数」の型になります。 gcd には治安が良い関数でほしいので、型シグネチャの部分を以下のように書き換えます

val gcd : int -> int -> Tot int

この例では残念ながら型検査を通りません。 よくよく考えると、例えばgcd -1 0などは停止せずに無限ループし続けるので当然です。 そもそもそんな入力は受け付けたくないので、関数の定義域を絞ります。

val gcd : a:int{ a > 0 } -> b:int{ b > 0 } -> Tot int

a:int{ a > 0 } は 「int 型のうち、 0 より大きい値」の型です。 この種の型は型の中に値の情報が現れており、値に依存しているので、依存型と呼ばれます。

今度は型の意味するところは正しいはず...なのですが、これでも型検査を通りません! 値域を正整数に限ればたしかに停止するのですが、残念ながら型検査器はその証明を思いつけていないのです。

そこで、人間がヒントを与える必要があります。

停止性の証明のためには

  • 再帰的な呼び出しごとに真に減少するが
  • 無限減少列はない ような値があることを型検査器に教えてあげればよいです。

例えば a+b とかはどうでしょう?再帰の度に小さくなっていそうだし、2 より大きいことは確定しているし、良さそうです。 このヒントを付けた型シグネチャが以下になります。

val gcd : a:int{a > 0} -> b:int{b > 0} -> Tot int (decreases %[a+b])

これでもまだ型検査が通りません。型検査器は

  • 関数中の Lt -> gcd b a の辺りで証明が回らないよ!?

などと、どこで検査に失敗したか教えてくれます。たしかに、 gcd a b の中で gcd b a が呼ばれているので、 このケースでは a+b が減っていません。そこで、 「a+b が変わらないときは b の値が減ってるはずだから、(a+b, b)のペアで考えてみて!」と教えることにします。

val gcd : a:int{a > 0} -> b:int{b > 0} -> Tot int (decreases %[a+b; b])

今度は無事に型がつきました。 これでこの関数が確実に停止することが保証されました。

実は x:int{x > 0} という型には pos という名前の alias が定義されています。よって、以下のように書くことも出来ます。

val gcd : a:pos -> b:pos -> Tot int (decreases %[a+b; b])

公約数を返す関数の型

さて、「2つの正整数を受け取ってその公約数を返す」関数の型を定義するために、 まず、 c が a と b の公約数かどうか判定する関数を定義します。

val is_common_factor : pos -> pos -> pos -> bool
let is_common_factor a b c = (a % c = 0) && (b % c = 0)

この関数を使って、欲しい仕様に対応する型シグネチャは以下のように書けます。

val gcd : a:pos -> b:pos -> Tot (c:pos{is_common_factor a b c})
              (decreases %[a+b; b])

なのですが、やっぱり型検査器は証明を見つけられません。 今度は

  • Gt -> gcd (a - b) b のケースで、 gcd (a - b) b が本当に a と b の公約数になってるかどうかわからないよ!

とのことです。

今後ちょいちょい出てくるので、説明の簡単化のために gcd (a - b) b の値を g と名づけます。 帰納法の仮定より g は a - b と b を割り切ることは即座にわかります。ですので、型検査器が苦労しているのはg が a を割り切るかどうかの確認ではないかと予測します。

ここで、「c が a と b の公約数だったら、 c は a+b を割り切る」という補題を仮定します。

val division_distributivity : a:pos -> b:pos -> c:pos{is_common_factor a b c}
        -> Lemma ((a + b) % c = 0)
let division_distributivity a b c = Math.Lemmas.modulo_distributivity a b c
// modulo_distributivity a b c = Lemma ((a + b) % c = (a + (b % c)) % c))

この補題より、 「g が (a-b) と b の公約数だったら、 g は a を割り切る」が言えるので、 必要な場所でコンパイラに教えてあげます。

val gcd : a:pos -> b:pos -> Tot (c:pos{is_common_factor a b c}) (decreases %[a+b; b])
let rec gcd a b =
    match compare_int a b with
    | Gt ->
        let g = gcd (a-b) b in
        division_distributivity (a-b) b g;
        g
    | Lt -> gcd b a
    | Eq -> a

これをコンパイルすると無事に型がつきました。gcd が公約数を返すことが証明されました。

エイリアス

type common_factor (a:pos) (b:pos) = c:pos{is_common_factor a b c}

なる型エイリアスを定義すれば、上の型を

val gcd : a:pos -> b:pos -> Tot (common_factor a b)

くらいにすっきりさせることができます。意味がわかりやすくなりました。

完成したプログラムはこちらです。

あとがき

なんとなく複雑な型を持つ言語の雰囲気が伝わったら幸いです。 ちなみに今日は新暦七夕です。織姫星と彦星にちなんでF starの記事を書きました。

余談

ここのところ型や形式手法についての話題が世間を賑わしていますね!

gfn 氏が静的型付きの組版用言語とその処理系の SATySFiを発表したり github.com

soutaro 氏が Ruby を型検査するシステムSteepを構築したり soutaro.hatenablog.com

バーチャル定理証明士が定理証明動画シリーズを開始したり www.youtube.com

みょん氏が型の強さについての紹介記事を書いてくれたり myuon.github.io

毎日興味深い話題がありドキドキがとまりません。

*1:この場合でもコンパイラはヒントを鵜呑みにせず、そのヒントが正しいかどうかを検査してくれるので正しさは保証されます。

型で仕様を表す

整数を受け取って整数を返す関数のつもりで、私が以下の関数を書いたとします。

// 仕様:この関数は整数を受け取って整数を返す関数だよ!
let my_clever_function x = "hello!"

上のプログラムは当然コンパイルできますし、私は仕様どおり正しい実装を書けた気がしています。何も問題ありません...ほんとに?

心配になったのでコメントに書かれていた仕様を型で書きなおすことにしました。

val my_clever_function : int -> int
let my_clever_function x = "hello!"

これをコンパイルしようとすると、コンパイラは以下のように間違いを指摘してくれます。

  • 整数型の式を書いてくれると思っていた場所に、文字列型の"hello!"という式が書いてあるよ!

たったしかに〜〜〜!!全然気づかなかった!!!

...というように、型を明示することで、式にその型を付けられるかどうかコンパイラがチェックしてくれます。 型には「コンパイラからも読める仕様」「コンパイラがチェックしてくれる仕様」としての一面があるのです。

Totally Runcible

There is an article in Qiita
It gives us no lore incognita
We call it the poem
The verse is just flowing
Ah Poet! You earn views like a cheetah!

 

参考記事

所感や私感を「ポエム」と呼ぶのをやめろ

LINQ遅くなさそう

注意

きちんとしたテストをしようと思ったのですが、途中でめんどくさくなりました。 条件を揃えたりILを読んだりしてないので余り意味はないかもしれませんが、結果だけここにおいときます。

結論

  • きちんとわかったこと
    • とくにないです
  • なんとなく思ったこと
    • LINQはボケーっと書くと確かにforより遅くなる
    • ちょっと工夫すればforやwhileと比べて遅くならないこともある?
    • debugビルドとreleaseビルドではそこまで速度の差が出ない
    • optimizationを有効にしないと悲惨

実験内容

以下の処理をする関数を幾つかの方法で書き、速度を比較。

処理

  • 与えられた整数列から
  • 十進表記中に"3"を含むものを除き
  • 5の倍数を除き
  • 十進表記中に現れる"57"を"91"に書き換え
  • 7の倍数を除き
  • その数から始まるコラッツ列が1に到達するまでの長さを求め
  • その和を返す

比較項目

  • LINQ/For文のどちらを使うか
  • Parallelにするかしないか
  • Optimizationを有効にするかしないか
  • 与えられた仕様を素朴に書き下すか/やや工夫するか

などの条件を変えて実行時間を比較。

条件

  • プログラム
    • github.com
    • 引数の整数列の長さ: 10000000
    • 5回テストして実行時間の平均を採用
    • 比較する関数が同じ値を返すっぽいことは dotnet testで確認
  • ビルドコマンド
    • dotnet build
  • 環境

実験結果

以下値はいずれも[秒]。 debugとreleaseの差はほとんどなかったので一部割愛。

素朴な実装のとき

Method Debug + Unoptimized Release+Optimized
LINQ 30.55 12.66
For文 24.13 06.89
ParallelLinq 13.69 05.76
ParallelFor 40.89 15.55

やや工夫したとき

Method Debug + Unoptimized Release+Optimized
LINQ 23.01 06.88
For文 23.10 07.20
ParallelLinq 13.45 05.43
ParallelFor 11.07 04.71

ちゃんとした比較実験にするためにしなければならないこと

  • 各メソッドの内容をきちんと考える。何を固定して何を動かすのか
  • IL(.netの中間言語)を読んで議論する

思ったこと

無駄の多いコードを書くと来世はきらら系4紙がない世界に転生してしまう 。

TeXの発音をWikipediaで調べてみた

TL; DR

  • 英語のように[tek]と発音する言語よりも、[tex] ([x]は喉の奥から出す「フ」の音)と発音する言語が2倍以上多い(ウィキ調べ)

前置き

gfn氏による関数型組版システム、SATySFiが話題になっている。

GitHub - gfngfn/SATySFi: A statically-typed, functional typesetting system

静的型と組版システムの組み合わせは衝撃的だ。プレゼンテーションから数日、今まで使われてきたLaTeXと、新時代の組版システムSATySFiの比較が盛んに行われている。

いつもの疑問

TeX/LaTeXが話題になるとき、人々はいつもの疑問を思い出す。

TeXをどう発音するか。 自分の見聞きした範囲だと日本では「テフ」派と「テック」派が二大勢力であり、かなり小数の「テヒ」派が三番手にいるという感じだ。 いづれも「TeX」という字面からは連想しづらいものである。

どの流派も「テ」までは一致しているが、語末の「X」の読み方で意見が分かれているのである。

本記事では日本語話者の便宜のため、メジャーと思われる十数言語についてWikipediaの記事「TeX」中の発音に関する記述を調べ、「X」の読み方についてどのような発音が多いのかまとめた。

注意

  • 以下の内容はWikipediaの記述を翻訳しただけであり、各言語話者がそのとおりに発音していると主張するわけではない。
  • どの発音が「正しい」のか、本記事では結論しない。

言語リスト(17ヶ語)

英語

The name TeX is intended by its developer to be /tɛx/, with the final consonant of loch or Bach.[53] The letters of the name are meant to represent the capital Greek letters tau, epsilon, and chi, as TeX is an abbreviation of τέχνη (ΤΕΧΝΗ – technē), Greek for both "art" and "craft", which is also the root word of technical. English speakers often pronounce it /ˈtɛk/, like the first syllable of technical.

TeXという名称は開発者にとってlochやBachの末尾の子音/x/を持つ/tɛx/のつもりだった。techinicalの語源でもある、ギリシャ語のτέχνη (ΤΕΧΝΗ – technē)の略称がTeXであり、綴りはタウ・イプシロン、カイの大文字を表していた。英語話者は/ˈtɛk/と発音する。これはtechnicalの最初の音節と同じ発音である。

アラビア語

TeXのルビにتخと振ってある。これは/t/ /x/を表す2子音である。

ベラルーシ語

TeX (чытаецца як Тэх...

ギリシャ語のτέχνη(技術)に由来し、Тэхと読まれる。

[tex]を意図しているようである。

チェコ語

Poznámka k výslovnosti: TeX se vyslovuje „tech“ (v angličtině též „tek“), protože jeho název není psán latinkou, ale řecky, takže poslední písmeno v názvu je řecký znak chí.

発音に関するメモ:Texはtechと発音される。(英語ではtekとも発音される。)なぜならラテン語ではなく、ギリシャ語だからである。最後の文字はギリシャ文字のχである。

とある。 [x]を意図しているようである。

ドイツ語

TeX ([tɛx], im deutschsprachigen Raum auch Zum [tɛç]),

Tex ([tɛx], ドイツ語圏では[tɛç]とも)

スペイン語

Donald Knuth explica en su obra The TeXbook que la palabra technology ("tecnología") tiene raíz griega y esta comienza por las letras τεχ. Por tanto, el nombre TeX en español se tiene que pronunciar [tej], y no [teks]. Ello se debe a que TeX no quiere decir TEX sino τεχ, acabado en la letra griega χ [ji].

... TeXスペイン語では[tej]と発音されなければならず、[teks]は誤りである。TeXTEXではなくτεχであり、最後の文字はギリシャ文字のχ[ji]であるからだ。

スペイン語のjは[x]で発音される。したがって、この記述は「TeXは[tex](テフ)と発音すべきである。なぜなら最後の文字はギリシャ文字のχ[xi]「ヒ」であるからだ」と読むべきだろう。

ペルシャ語

تک

/t/ /k/を表す二子音である。

フランス語

TeX vient de τεχ, début du mot τέχνη (« art, science », en grec ancien), et se prononce /tɛx/ ou /tɛk/, au choix.

TeXギリシャ語τέχνη(技術)のτεχに由来し、好みにより/tɛx/とも/tɛk/とも発音される。

韓国語

TeX(그리스어: IPA: [ˈtɛx] 테흐[], 영어: IPA: [ˈtɛk] 텍[])은 ...

TeX(ギリシャ語: IPA:[ˈtɛx] 테흐, 英語: IPA: [ˈtɛk] 텍)は ...

ギリシャ語読みでは /tehɯ/、英語読みでは/tek/であるとハングルで発音が記されている。

イタリア語

TEX, scritto anche TeX e pronunciato alla greca come tech (la "ch" è pronunciata come nella parola tedesca "Ach" o in quella scozzese "Loch"), è

TEX -- TeXとも表記される。ギリシャ語に習い、techと発音される。(ドイツ語のAch, スコットランド語のLochのch) -- は...

[tex]として記述されている。

オランダ語

TeX (officieel geschreven als TEX en uitgesproken als tech, dus met Griekse chi) is ...

TeX(正式にはTEXと書かれ、ギリシャ文字のchiのようにtechと発音される)は...

オランダ語版のChi(letter)の記事には

De chi wordt uitgesproken als de stemloze palatale fricatief /ch/

Chiは無声硬口蓋摩擦音/ch/で発音される。

との記述があるので、上の記述はIPA表記では[teç]を意図しているものであるとわかる。

ポーランド語

TeX (wymowa IPA: /tɛx/ jak gr.)

Tex 発音 IPA: /tɛx/ ギリシャ式に

jakの訳出に自信がないが、語源がギリシャ語であり、それに習って発音すると述べていることは間違いないようである。

ルーマニア語

TeX (AFI /tɛx/ ca în greacă sau /tɛk/ ca în engleză...)...

TeX (ギリシャ式に /tɛx/ あるいは英語式に /tɛk/...)...

ロシア語

Название произносится как «тех» (от греч. τέχνη — «искусство», «мастерство»)

名前は«тех»と発音される。(ギリシャ語のτέχνηに由来)

ロシア語ではхは[x]と発音されるから[tex]派である。

スウェーデン語

Det är meningen att namnet TeX ska uttalas "tech", där "ch" motsvarar ljudet i slutet av tyskans "ach".

... ドイツ語の"ach"の"ch"のように "tech"と発音する。

[tex]派である。

フィンランド語

TeX tulisi lausua ”teh”. X tarkoittaa tässä kreikkalaista kirjainta χ (khi).

Texは"teh"と発音すべきである。 Xはギリシャ文字のχ(khi)を現している。

tullaって「すべき」と訳して大丈夫ですか...?

Finnish sound structure: phonetics, phonology, phonotactics and prosodyの28ページの記述を見る限り、[teh]を意図した記述のようである。

中国語

TEX这个词的标准发音为/tɛx/,其中/x/相当于普通话“赫”字的声母,或者苏格兰语“loch”一词中“ch”的发音(X其实是希腊字母 χ)。音译“泰赫”。在英语和法语中实际通常读作/tɛk/,音译“泰克”。

TEXという語の標準的な発音は/tɛx/である。この/x/は中国語の“赫”の子音やスコットランド語の"loch"の"ch"の発音に相当する(Xはギリシャ文字のχである)。音訳すると“泰赫”である。英語とフランス語では通常/tɛk/と読まれる。音訳すると“泰克”である。

まとめ

以上の調査の結果に日本語の「テフ」・「テック」を加えた表を以下に示す。

発音 音声ファイル1 備考
[x] 14
[k] 6 英語・ペルシャ語・日本語。また、チェコ語・韓国語・中国語で、英語では[k]との記述あり。
[ç] 2 ドイツ語・オランダ語
[h] 2 韓国語・フィンランド
[ɸ] 1 日本語「テフ」

[x]が圧倒的大多数であり、[k]が二番手として続く。'X'の発音に[ɸ]をあてている言語は調査した中では日本語だけであった1。また、[k]のみが破裂音であり、他の全ての音は摩擦音であった。

表中の音声ファイルは以下より。

ファイル:Voiceless velar plosive.ogg - Wikipedia

ファイル:Voiceless velar fricative.ogg - Wikipedia

ファイル:Voiceless palatal fricative.ogg - Wikipedia

ファイル:Voiceless glottal fricative.ogg - Wikipedia

ファイル:Voiceless bilabial fricative.ogg - Wikipedia


  1. そもそも[ɸ]を持っている言語自体がかなり少ない。

  2. 音声ファイルの[h]の発音に若干pharyngealが入ってる気がする

C#でC++のcinっぽいの

作った。

class cin {
    private static Queue<string> tokens;
    static cin () {
        string line;
        tokens = new Queue<string> ();
        while ((line = Console.ReadLine ()) != null) {
            foreach (var token in line.Split (' ')) {
                tokens.Enqueue (token);
            }
        }
    }
    public static implicit operator int (cin cin) => int.Parse (cin.tokens.Dequeue ());
    public static implicit operator string (cin cin) => cin.tokens.Dequeue ();

    public void Deconstruct (out cin o1, out cin o2) => (o1, o2) = (this, this);
    public void Deconstruct (out cin o1, out cin o2, out cin o3) =>
        (o1, o2, o3) = (this, this, this);
    public void Deconstruct (out cin o1, out cin o2, out cin o3, out cin o4) =>
        (o1, o2, o3, o4) = (this, this, this, this);
    public void Deconstruct (out cin o1, out cin o2, out cin o3, out cin o4, out cin o5) =>
        (o1, o2, o3, o4, o5) = (this, this, this, this, this);
    public void Deconstruct (out cin o1, out cin o2, out cin o3, out cin o4, out cin o5, out cin o6) =>
        (o1, o2, o3, o4, o5, o6) = (this, this, this, this, this, this);
    public void Deconstruct (out cin o1, out cin o2, out cin o3, out cin o4, out cin o5, out cin o6, out cin o7) =>
        (o1, o2, o3, o4, o5, o6, o7) = (this, this, this, this, this, this, this);
    public void Deconstruct (out cin o1, out cin o2, out cin o3, out cin o4, out cin o5, out cin o6, out cin o7, out cin o8) =>
        (o1, o2, o3, o4, o5, o6, o7, o8) = (this, this, this, this, this, this, this, this);
}

こんな感じに使う。

int N                      = cin;
string name                = cin;
(int A, string str, int B) = cin;

castをabuseすると治安の悪いコードが書ける。

各種ズンドコ節のズンドコ部分の比較

取り急ぎなので間違っていたらごめんなさい><

比較

タイトル 歌手 発表年 ズンドコ部分 備考
海軍小唄 不詳 1945以前 トコズンドコズンドコ 流行歌
街の伊達男 田端義夫 1947年 トコズンドコズンドコ 長調
東京ズンドコ 安城美智子 鈴村一郎 1951年 トコ東京ズンドコズンドコ 海軍小唄に近いメロディ
アキラのズンドコ節 小林旭 1960年 ズン・ズン・ズンドコ ズンドコ部分の後に10小節ほど別メロディが挿入されている
ドリフのズンドコ節 ザ・ドリフターズ 1969年 ズンズンズンズンズンズンドコ ズンドコ部分のほかは海軍小唄にほぼ同じメロディ
零心会のズンドコ節 劇男零心会 1986年 ズンズン・ズンズン・ズンズンドコ ズンドコ部分の後に10小節ほど別メロディ。 サビ最後直前にタメ。
きよしのズンドコ節 氷川きよし 2002年 ズン・ズンズンズンドコ 演歌風の前奏付き
zung zung funky music ORANGE RANGE 2004年 ズンズンファンキーミュージック ラップ調
Zoun-Doko Bushi Les Romanesque 2011年 ズンズンズンズンズンズンドコ フランス語 ドリフのズンドコ節に近い

結論

「ズン・ズンズン・ズンドコ」は少数派! ひょっとしたらきよしのズンドコ節が初出?