Next: Functions and Variables for Predicates, Previous: Functions and Variables for Properties, Up: Maximas Database [Contents][Index]
文脈context_1, …, context_nをアクティベートします。
これらの文脈に関する事実は、演繹し情報を検索するために利用可能となります。
これらの文脈に関する事実は、facts ()によってリストされません。
変数activecontextsは、
activate関数を使ってアクティブになった文脈のリストです。
デフォルト値: []
変数activecontextsは、
アクティブである文脈と対照的に、
activate関数を使ってアクティブになった文脈のリストです。
ゆえに、それらは現在の文脈の部分文脈です。
asksignがコールされた時、
askexpは、asksignがテストしている式です。
以前は、control-AでMaximaブレイクに入ることによって、
ユーザーがaskexpを検査することができました。
askinteger (expr, integer)は、
assumeデータベースから、exprが整数かどうかを決定しようとします。
そうでなく、もし決定できなければ、askintegerはユーザーに入力を促し、
可能ならばデータベースに情報をインストールしようとします。
askinteger (expr)は、
askinteger (expr, integer)と同値です。
同様に、
askinteger (expr, even)やaskinteger (expr, odd)は、
それぞれ、exprが偶数か奇数か、決定しようとします。
最初に、指定された式が正か負かゼロか決定しようとします。
できなければ、演繹を完了するのに必要な質問をユーザーに尋ねます。
ユーザーの答えは、現在の計算の演繹のため、データベースに記録されます。
asksignの戻り値は、pos, negもしくはzeroのいずれか１つです。
述語論理pred_1, …, pred_nを現在の文脈に追加します。
もし述語論理が現在の文脈と矛盾していたり、冗長だったりしたなら、文脈に追加されません。
文脈はassumeがコールされる毎に述語論理を累積していきます。
assumeは、文脈に追加された述語論理を要素に持つリストか、
適用されたアトムredundantもしくはinconsistentを返します。
述語論理pred_1, …, pred_nは
関係演算子< <= equal notequal >= >を持つ式のみ許されます。
述語論理はリテラル等号=やリテラル不等号#の式は使えません。
integerpのような述語関数も使えません。
形式pred_1 and ...and pred_nの合成された述語論理が認識されます。
しかし、pred_1 or ... or pred_nは認識されません。
もしpred_kが関係述語論理なら、not pred_kは認識されます。
形式not (pred_1 and pred_2)の式や
not (pred_1 or pred_2)は認識されません。
Maximaの推論メカニズムはそれほど強くありません;
isによって決定されない多くの明らかな結果があります。
これは既知の弱みです。
assumeは複素数を伴う述語論理を扱いません。
もし述語論理が複素数を含むなら、assumeはinconsistentかredundantを返します。
assumeは引数を評価します。
isやfacts, forget, context, declareも参照してください。
例:
(%i1) assume (xx > 0, yy < -1, zz >= 0); (%o1) [xx > 0, yy < - 1, zz >= 0] (%i2) assume (aa < bb and bb < cc); (%o2) [bb > aa, cc > bb] (%i3) facts (); (%o3) [xx > 0, - 1 > yy, zz >= 0, bb > aa, cc > bb] (%i4) is (xx > yy); (%o4) true (%i5) is (yy < -yy); (%o5) true (%i6) is (sinh (bb - aa) > 0); (%o6) true (%i7) forget (bb > aa); (%o7) [bb > aa] (%i8) prederror : false; (%o8) false (%i9) is (sinh (bb - aa) > 0); (%o9) unknown (%i10) is (bb^2 < cc^2); (%o10) unknown
デフォルト値: true
assumescalarは、
nonscalarp (expr)がfalseであるような式exprが、
ある変換に関してスカラーのように振る舞うと仮定されるかどうかを決めるのを助けます。
Let
exprがリストや行列以外の任意の式を表してるとし、
[1, 2, 3]が任意のリストや行列を表しているとすると、
もしassumescalarがtrue、
もしくはscalarp (expr)がtrue、
もしくはconstantp (expr)がtrueなら、
expr . [1, 2, 3]は、[expr, 2 expr, 3 expr]をもたらします。
もしassumescalarがtrueなら、
そんな式は可換演算子に関してだけスカラーのように振る舞いますが、
非可換乗算.に関してはそうは振る舞いません。
assumescalarがfalseの時
そんな式は、非スカラーのように振る舞います。
assumescalarがallの時、
そんな式は、上でリストされた演算子すべてに関してスカラーのように振る舞います。
デフォルト値: false
assume_posがtrueで、
パラメータxの符号が現在の文脈や他の考慮から決定できない時、
signやasksign (x)は、trueを返します。
これは、integrateや他の計算から起こるような、
自動生成されるasksign問い合わせを事前に防ぐことができます。
デフォルトでは、パラメータはsymbolp (x)もしくは
subvarp (x)のようなxです。
パラメータとして考えられる式のクラスは、
変数assume_pos_predを介して、ある程度変えることができます。
signとasksignは、
式の中のオペランドの符号から式の符号を演繹しようとします。
例えば、もしaやbがともに正なら、
a + bも正です。
しかしながら、asksign問い合わせすべてを迂回する方法はありません。
特に、asksign引数が、差x - yもしくは
対数log(x)の時、
たとえassume_posがtrueで、assume_pos_predが
引数すべてにtrueを返す関数であっても、
asksignは、いつもユーザーからの入力を要請します。
デフォルト値: false
assume_pos_predが関数名や、引数xのラムダ式に割り当てられている時、
その関数は、
xが、assume_posのためのパラメータと考えられるかどうかを決定するために
コールされます。
assume_posがfalseの時、
assume_pos_predは、無視されます。
assume_pos_pred関数は、引数xでsignとasksignによってコールされます。
ここで、xはアトム、添字付き変数、関数コール式のいずれかです。
もしassume_pos_pred関数がtrueを返すなら、
xは、assume_posのためのパラメータと考えられます。
デフォルトでは、パラメータは、symbolp (x)もしくはsubvarp (x)のようなxです。
assumeとassume_posも参照してください。
例:
(%i1) assume_pos: true$
(%i2) assume_pos_pred: symbolp$
(%i3) sign (a);
(%o3) pos
(%i4) sign (a[1]);
(%o4) pnz
(%i5) assume_pos_pred: lambda ([x], display (x), true)$
(%i6) asksign (a);
x = a
(%o6) pos
(%i7) asksign (a[1]);
x = a
1
(%o7) pos
(%i8) asksign (foo (a));
x = foo(a)
(%o8) pos
(%i9) asksign (foo (a) + bar (b));
x = foo(a)
x = bar(b)
(%o9) pos
(%i10) asksign (log (a));
x = a
Is a - 1 positive, negative, or zero?
p;
(%o10) pos
(%i11) asksign (a - b);
x = a
x = b
x = a
x = b
Is b - a positive, negative, or zero?
p;
(%o11) neg
デフォルト値: initial
contextは、assumeとforgetによって保守される事実の集まりの名前です。
assumeは、contextと名付けられた集まりに事実を追加する一方、
forgetは、事実を取り除きます。
contextを名前fooにバインドすることは、
現在の文脈をfooに変えます。
もし指定された文脈fooがまだ存在しないなら、
newcontextのコールによって自動的に生成されます。
指定された文脈は自動的にアクティベートされます。
文脈メカニズムの一般的な記述に関しては、contextsを参照してください。
デフォルト値: [initial, global]
contextsは、
現在アクティブな文脈を含んでいる、現在存在する文脈のリストです。
文脈メカニズムは、ユーザーが 文脈と呼ばれる事実の集まりにバインドし、名付けることを可能にします。 一旦これがなされると、ユーザーは、 文脈を単にアクティベートしたりデアクティベートすることで、 たくさんの数の事実をMaximaに仮定させたり忘れさせたりできます。
任意のシンボルのアトムは、文脈となりえ、
その文脈の中に含まれた事実は、
forgetをコールすることで１つ１つ破壊されるまで、
あるいは、それらが属する文脈を破壊するためにkillをコールすることで、全体として破壊されるまで、記憶装置に保持されます。
文脈は階層的に存在します。
その根はいつも文脈globalであり、
文脈globalは、いくつかの関数が必要とするMaximaについての情報を含みます。
アクティブな文脈の部分文脈である任意の文脈の中の事実すべてそうであるように、
与えられた文脈の中では、
その文脈の中の事実すべては、「アクティブ」（それらが演繹や探索に使われるという意味）
です。
新鮮なMaximaが起動された時、
ユーザーは、initialと呼ばれる文脈の中にいます。
それは、部分文脈としてglobalを持ちます。
facts, newcontext,
supcontext, killcontext, activate, deactivate, assume, forgetも参照してください。
特定の文脈context_1, …, context_nをデアクティベートします。
もしitemが文脈の名前なら、
facts (item)は指定された文脈のfactsのリストを返します。
もしitemが文脈の名前でなければ、
facts (item)は現在の文脈の中で、
itemについて知っているfactsのリストを返します。
異なる文脈中のアクティブなfactsはリストされません。
facts ()（すなわち引数なし）は現在の文脈をリストします。
assumeで規定された述語論理を取り除きます。
述語論理は以前に規定されたものと同値の（必ずしも同一である必要なない）式です。
forget (L)（Lは述語論理のリスト）は、
リスト上のそれぞれの項目を忘れます。
assumeデータベースの中の事実から述語論理exprが確かか否かを決定
しようとします。
もし述語論理が確かにtrueもしくはfalseなら、
isは、それぞれtrueもしくはfalseを返します。
そうでなければ、戻り値は、グローバルフラグprederrorに依存します。
prederrorがtrueの時、
isはエラーメッセージを出力します。
そうでなければ、isはunknownを出力します。
ev(expr, pred)
(対話プロンプトでは、expr, predと書けます)
は、is(expr)と同値です。
assume, facts, maybeも参照してください。
例:
isは述語論理の評価を引き起こします。
(%i1) %pi > %e; (%o1) %pi > %e (%i2) is (%pi > %e); (%o2) true
isは、assumeデータベースから述語論理を演繹しようとします。
(%i1) assume (a > b); (%o1) [a > b] (%i2) assume (b > c); (%o2) [b > c] (%i3) is (a < b); (%o3) false (%i4) is (a > c); (%o4) true (%i5) is (equal (a, c)); (%o5) false
もしisがassumeデータベースから述語論理を証明もしくは否定できなかったら、
グローバルフラグprederrorがisの振る舞いを決めます。
(%i1) assume (a > b); (%o1) [a > b] (%i2) prederror: true$ (%i3) is (a > 0); Maxima was unable to evaluate the predicate: a > 0 -- an error. Quitting. To debug this try debugmode(true); (%i4) prederror: false$ (%i5) is (a > 0); (%o5) unknown
文脈context_1, …, context_nを消します。
もし文脈の１つが現在の文脈なら、
新しい文脈は、
消されなかった現在の文脈の最初の利用可能な部分文脈になるでしょう。
もし最初の利用可能な消されなかった文脈がglobalなら、
initialが代わりに使われます。
もしinitial文脈が消されたら、
新しい、空のinitial文脈が生成されます。
killcontextは、現在アクティブな文脈を消すことを拒否します。
なぜなら、それは現在の文脈の部分文脈、もしくは
関数activateの使用によってアクティブになっているから。
killcontextは、引数を評価します。
killcontextは、doneを返します。
述語論理exprがassumeデータベースの事実から正しいかどうかを
決定しようとします。
もし述語論理が確かにtrueもしくはfalseなら、
maybeは、それぞれtrueもしくはfalseを返します。
そうでなければ、maybeはunknownを返します。
maybeは、prederror: falseでのisと関数的に同値です。
しかし、prederrorに値を実際に割り当てることなく結果が計算されます。
assume, facts, isも参照してください。
例:
(%i1) maybe (x > 0); (%o1) unknown (%i2) assume (x > 1); (%o2) [x > 1] (%i3) maybe (x > 0); (%o3) true
nameと呼ばれる新しい、空の文脈を生成します。
nameは、唯一の部分文脈としてglobalを持ちます。
新しく生成された文脈は現在アクティブな文脈になります。
newcontextは、引数を評価します。
newcontextは、nameを返します。
現在のデータベースの事実に基づいてexprの符号を決定しようとします。
以下の答えの１つを返します;
pos (positive), neg (negative), zero, pz
(正もしくはゼロ), nz (負もしくはゼロ), pn (正もしくは負),
or pnz (正、負もしくはゼロ、すなわちなにもわからない).
nameと呼ばれる新しい文脈を生成します。 nameは、部分文脈としてcontextを持ちます。 contextは存在しなければいけません。
もしcontextが指定されないなら、 現在の文脈が仮定されます。
Next: Functions and Variables for Predicates, Previous: Functions and Variables for Properties, Up: Maximas Database [Contents][Index]