問題タブ [proof]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
graph - 二部連結グラフ証明
友人が私に真実のように思われる推測を提示しましたが、私たちのどちらも証明を思い付くことができません. 問題は次のとおりです。
|U|<|V| のように、互いに素な空でない頂点セット U と V をもつ接続された 2 部グラフが与えられ、すべての頂点が U または V のいずれかにあり、同じセット内の 2 つの頂点を接続するエッジはありません。次数(a)>次数(b)となるように頂点a∈Uとb∈Vを接続するエッジが少なくとも1つ存在する
U に V の次数よりも高い次数を持つ頂点が少なくとも 1 つあることを証明するのは簡単ですが、それらを接続するエッジを持つペアが存在することを証明するのは困難です。
theory - なぜすべてのLL(1)文法がLR(1)なのですか?
LL(1)文法もLR(1)であることは広く知られている事実ですが、これの厳密な証拠はどこにも見つからないようです。証明の概要をいくつか聞いたことがあります(たとえば、LL(1)文法では、一度に1つのトークンから生成が決定されるため、LR(1)文法では、決定前にはるかに多くの入力をスキャンできます)作られています)。しかし、コンパイラに関する2つの教科書を調べ、解析してGoogleですばやく検索した後、この事実のより正式な証明を突き止めることができないようです。
誰かがこの証拠、または少なくともそれを見つける場所を知っていますか?
c# - コルーチンの動作を証明する
Mono Continuations (非常に奇妙な経験) に基づいて (演習として) コルーチンの実装を作成しました。その正しさを証明するために取るべきいくつかの方法/アプローチは何ですか?
theory - 停止問題が NP 困難であることの証明は?
NP、NP-hard、および NP-complete の定義に関するこの質問への回答で、Jason は次のように主張しています。
停止問題は古典的な NP 困難問題です。これは、プログラム P と入力 I が与えられた場合、停止するかという問題です。これは決定問題ですが、NP にはありません。あらゆる NP 完全問題がこの問題に還元できることは明らかです。
停止問題は直感的に NP のどの問題よりもはるかに「難しい」問題であることに同意しますが、停止問題が NP 困難であるという正式な数学的証明を正直に思いつくことはできません。特に、NP のすべての問題 (または少なくとも既知の NP 完全問題) のインスタンスから停止問題への多項式時間多対 1 マッピングを見つけることができないようです。
停止問題が NP 困難であるという簡単な証明はありますか?
algorithm - 二分木の実装
次のテキストは、アルゴリズムブックの抜粋です。
リンクリストで一般的な長方形のボックスを使用して二分木を描画することもできますが、実際にはグラフであるため、ツリーは通常、線で結ばれた円として描画されます。また、ツリーを参照するときにNULLリンクを明示的に描画しません。これは、Nノードを持つすべてのバイナリツリーがN +1NULLリンクを必要とするためです。
私の質問は、N個のノードを持つすべての二分木がN +1個のヌルリンクを必要とすることを著者が何を意味するのかということです。著者はどのようにしてN+1番号を付けましたか?
lisp - Lisp関数を「純粋」と宣言する機能は有益でしょうか?
私は最近Haskellについてたくさん読んでいます、そしてそれが純粋に関数型言語であることから得られる利点。(私はLispのモナドについて議論することに興味がありません)(少なくとも論理的に)副作用のある関数を可能な限り分離することは私にとって理にかなっています。私はsetf
他の破壊的な関数をたくさん使ってきました、そして私はLispと(ほとんどの)その派生物でそれらの必要性を認識しています。
どうぞ:
(declare pure)
コンパイラの最適化に役立つ可能性があるものはありますか?それとも、すでに知っているので、これは論点ですか?- 宣言は、関数やプログラム、または少なくとも純粋であると宣言されたサブセットを証明するのに役立ちますか?それとも、プログラマー、コンパイラー、および証明者にはすでに明らかであるため、これも不要なものですか?
- 他に何もないとしても、コンパイラーがこの宣言で関数の純粋さを強制し、Lispプログラムの可読性/保守性を高めることはプログラマーにとって有用でしょうか?
- これは意味がありますか?それとも私は今考えることすらできないほど疲れていますか?
ここで洞察をいただければ幸いです。コンパイラの実装または証明可能性に関する情報は大歓迎です。
編集
明確にするために、私はこの質問をCommonLispに限定するつもりはありませんでした。それは明らかに(私が思うに)特定の派生言語には当てはまりませんが、他のLispのいくつかの機能がこの種の機能をサポートする(またはサポートしない)傾向があるかどうかも興味があります。
algorithm - 2つのエッジに対応する放物線が最大で2点で交差することを帰納法で証明するにはどうすればよいですか?
互いに交差している放物線がたくさんあります。これらの放物線の上部セグメントからリストSを生成しています。放物線の対応する2つのエッジは、最大で2点で交差するため、リストSには最大で2n –1個のアイテムを含めることができます。
これを誘導で証明したい。私が考えることができるのはこれです:
f(x)≤2n–1であると仮定します。
基本ケースはn=1、f(1)≤2・1 – 1であるため、f(1)<=1です。
次に、 n = kが成り立つと仮定します。したがって、 f(k)≤2k–1です。
n = k + 1の場合、 f(k + 1)≤2(k + 1) –1が成り立つことを示すことができます。
私はそのように続けることになっていますか、例えば、n = k + 2、n = k + 3、…?このまま続けると、誘導で証明したということですか?
math - ステートメントの大きな O の証明
n^k
それがO(2^n)
すべての人に当てはまることを証明するのに苦労していますk
。lg2
両面取ってみたのk*lgn=n
ですが、これは違います。これを他にどのように証明できるかわかりません。
algorithm - 疑似コードの誘導による証明
疑似コードで帰納法による証明を使用する方法がよくわかりません。数式で使用するのと同じようには機能しないようです。
配列内の k で割り切れる整数の数を数えようとしています。
これが正しいことをどのように証明しますか?ありがとう