小编Sar*_*lle的帖子

问题如下:考虑三个输入A,B,C,找到一个带AND,OR和NOT门的布尔电路,使输出不是(A),不是(B),不是(C)最多使用2 NOT大门.

我想找一个带prolog的电路.我的想法是计算一个带有函数的谓词"可访问",并说它是否存在计算f的电路.

我有以下谓词:

not([],[]).
not([H|T],[G|S]) :- G #=# 1-H, not(T,S).

or([],[],[]).
or([0|T],[0|S],[0|R]) :- or(T,S,R).
or([1|T],[0|S],[1|R]) :- or(T,S,R).
or([1|T],[1|S],[1|R]) :- or(T,S,R).
or([0|T],[1|S],[1|R]) :- or(T,S,R).

and([],[],[]).
and([1|T],[1|S],[1|R]) :- and(T,S,R).
and([0|T],[1|S],[0|R]) :- and(T,S,R).
and([1|T],[0|S],[0|R]) :- and(T,S,R).
and([0|T],[0|S],[0|R]) :- and(T,S,R).

accessible(_,_,0) :- !,fail.
accessible([0,1,0,1,0,1,0,1],[12],_) :- !.
accessible([0,0,1,1,0,0,1,1],[11],_) :- !.
accessible([0,0,0,0,1,1,1,1],[10],_) :- !.
accessible(F,L,C) :- CC is C-1, or(G,H,F), accessible(G,M,CC), accessible(H,N,CC), L=[0, [M,N]].
accessible(F,L,C) :- CC is C-1, and(G,H,F), accessible(G,M,CC), accessible(H,N,CC), L=[1,[M,N]].
accessible(F,L,C) :- CC is C-1,  not(F,X), accessible(X,M,CC), L=[2,M].

我想计算11,12之间的函数xor,所以我尝试了以下目标:accessible([0,1,1,0,0,1,1,0],X,4).

但prolog运行了一段时间才得到了好的答案.我想知道如何改进程序以使其更快.

PS如何使用GNU prolog打印没有ASCII代码的字符串？

我试图在Coq中形式化群组.我希望尽可能地一般.我尝试做某事,但我对此并不满意.我发现了不同的实现,我不知道选择哪一个.

例如,我发现了这个:

https://people.cs.umass.edu/~arjun/courses/cs691pl-spring2014/assignments/groups.html

(* The set of the group. *)
Parameter G : Set.

(* The binary operator. *)
Parameter f : G -> G -> G.

(* The group identity. *)
Parameter e : G.

(* The inverse operator. *)
Parameter i : G -> G.

(* For readability, we use infix <+> to stand for the binary operator. *)
Infix "<+>" := f (at level 50, left associativity).

(* The operator [f] is associative. *)
Axiom assoc : …

我正在关注软件基金会这本书,我在名为"Imp"的章节.

作者公开了一种小语言,如下所示:

Inductive aexp : Type :=
  | ANum : nat -> aexp
  | APlus : aexp -> aexp -> aexp
  | AMinus : aexp -> aexp -> aexp
  | AMult : aexp -> aexp -> aexp.

以下是评估这些表达式的函数:

Fixpoint aeval (a : aexp) : nat :=
  match a with
  | ANum n ? n
  | APlus a1 a2 ? (aeval a1) + (aeval a2)
  | AMinus a1 a2 ? (aeval a1) - (aeval a2)
  | AMult a1 a2 ? (aeval …

我有几个模块实现相同的接口.我想根据命令行中给出的一个参数只加载该模块中的一个.

我在考虑使用一流的模块,但问题是我想在模块实例化之前执行一些功能.

目前我有这个:

module Arch = (val RetrolixAbstractArch.get_arch() : RetrolixAbstractArch.AbstractArch)


let get_arch () =
  let arch = Options.get_arch() in
  if arch = "" then
    Error.global_error "During analysis of compiler's architecture"
               "No architecture specified"
  else
    if arch = "mips" then
      ( module MipsArch : AbstractArch)
    else
    Error.global_error "During analysis of compiler's architecture"
               (Printf.sprintf "Architecture %s not supported or unknown" arch)      

但由于命令行尚未解析,请Options.get_arch给我空字符串.

我想在执行此函数之前实现命令行解析(不在函数中添加解析).可能吗 ？我应该找到另一种方法来实现这一目标吗？

问题出在标题中.我想做这样的事情:

myfunc<- pexp
plot(function(x) myfunc(x, 0.5))

我想在我的脚本中调用几个作为参数给出的函数.我想使用foreach而不是一堆if-then-else语句:

假设我以这种方式调用我的脚本:

R --slave -f script.R --args plnorm pnorm 

我想做这样的事情:

#only get parameters after --args
args<-commandArgs(trailingOnly=TRUE)
for i in args {
    plot(function(x) i(x,param1,param2))
}

下面的章节给出的例子GeneralRec Chlipala的书,我想写归并算法.

这是我的代码

Require Import Nat.

Fixpoint insert (x:nat) (l: list nat) : list nat :=
  match l with
  | nil => x::nil
  | y::l' => if leb x y then
              x::l
            else
              y::(insert x l')
  end.

Fixpoint merge (l1 l2 : list nat) : list nat :=
  match l1 with
  | nil => l2
  | x::l1' => insert x (merge l1' l2)
  end.

Fixpoint split (l : list nat) : list nat * list nat :=
  match l …

使用以下代码片段

use std::mem;

fn main() {
   println!("size Option(bool): {} ({})", mem::size_of::<Option<bool>>(), mem::size_of::<bool>());
   println!("size Option(u8): {} ({})", mem::size_of::<Option<u8>>(), mem::size_of::<u8>());
   println!("size Option(u16): {} ({})", mem::size_of::<Option<u16>>(), mem::size_of::<u16>());
   println!("size Option(u32): {} ({})", mem::size_of::<Option<u32>>(), mem::size_of::<u32>());
   println!("size Option(u64): {} ({})", mem::size_of::<Option<u64>>(), mem::size_of::<u64>());
   println!("size Option(u128): {} ({})", mem::size_of::<Option<u128>>(), mem::size_of::<u128>())
}

我在 64 位机器上看到：

size Option(bool): 1 (1)
size Option(u8): 2 (1)
size Option(u16): 4 (2)
size Option(u32): 8 (4)
size Option(u64): 16 (8)
size Option(u128): 24 (16)

因此开销不是恒定的并且会上升到8字节。我想知道为什么存储标签的开销不只是一个字节？我还想知道编译器选择什么表示形式？