有基于高阶逻辑(HOL)的编程语言和定理证明器.例子包括Twelf,lambda prolog,Isabelle.例如,Twelf既是编程语言又是定理证明者,而Isabelle主要是一个定理证明者,但是对于Isabelle代码提取是可用的.
我正在寻找一种基于haskell的HOL编程语言.原因是我非常喜欢lambda prolog,但它并不是一种实用的编程语言.Lambda prolog缺少标准库,与外部库的接口似乎并不简单.问题是如果你需要一些功能,比如为文本文件编写解析器,你就不能与haskell的许多可用现有库接口,而且,没有标准库,所以你从头开始.
今天我遇到了Caledon编程语言,它似乎是作为硕士论文实现的.从github页面:
Caledon是一种依赖类型,多态,高阶逻辑编程语言.
这很有趣,因为它是用haskell编写的,所以它应该很容易扩展并与现有的haskell库接口.但似乎该项目处于初期阶段,我不确定是否实现了输入输出(IO).由于我今天才了解卡利多,我想我可能错过了一些其他项目.(顺便说一句,我对像prolog这样的标准逻辑编程语言不感兴趣).
除了Caledon之外,是否有基于高阶逻辑的编程语言在haskell中实现？
(我要求"在haskell中实现",因为它很容易连接可以提取到haskell或在haskell中实现的编程语言.例如,Agda编程语言可以编译为haskell代码,haskell库可以方便地使用如果你知道如何使用haskell库是非常容易的.我相信的许多其他编程语言(例如,ATS)只提供最小的公共分母,这是一个基于C的外部函数接口(FFI).在我看来,连接相当麻烦两个更高级的编程语言通过它们各自的基于C的FFI接口.因此,似乎是"它应该在haskell中实现"的一部分.此外,作为旁注,一些用户过去曾因为我将Agda描述为编程语言而投降,但当然这不是真的,即考虑库里 - 霍华德)
我使用实施实验OOP语言和现在的基准垃圾收集存储性能基准测试.现在我想检查/打印下面的小深度基准(n = 2,3,4,..).
通过该buildTreeDepth方法生成树(具有4个子节点的林).代码如下:
import java.util.Arrays;
public final class StorageSimple {
private int count;
private int seed = 74755;
public int randomNext() {
seed = ((seed * 1309) + 13849) & 65535;
return seed;
}
private Object buildTreeDepth(final int depth) {
count++;
if (depth == 1) {
return new Object[randomNext() % 10 + 1];
} else {
Object[] arr = new Object[4];
Arrays.setAll(arr, v -> buildTreeDepth(depth - 1));
return arr;
}
}
public Object benchmark() { …我想找到关于代码质量的5个顶级编程R包.
看看我想学习如何改进的代码.遗憾的是,许多包装都没有很好的编程.最近我越来越多地使用Map(),Reduce()和Filter()函数,这已经产生了更好的代码.
有充分的理由,我想在leksah IDE中暂时关闭丢失类型级别签名的警告.
我将标志更改为ghc cabal文件,当我从控制台运行"cabal install"时,警告不存在.
但是,如果我在leksah IDE中构建相同的项目,则仍会显示警告.
如何在leksah IDE中关闭"警告:没有类型签名的顶级绑定:"？
"checkSimple"获取宇宙U的元素u,并检查是否(nat 1)可以转换为给定u的agda类型.返回转换结果.
现在我尝试编写一个控制台程序并从命令行获取"someU".
因此,我将"checkSimple"的类型更改为包含(u:Maybe U)作为参数(可能因为来自控制台的输入可以是"无").但是我无法获取键入检查的代码.
module CheckMain where
open import Prelude
-- Install Prelude
---- clone this git repo:
---- https://github.com/fkettelhoit/agda-prelude
-- Configure Prelude
--- press Meta/Alt and the letter X together
--- type "customize-group" (i.e. in the mini buffer)
--- type "agda2"
--- expand the Entry "Agda2 Include Dirs:"
--- add the directory
data S : Set where
nat : (n : ?) ? S
nil : S
sTo? : S ? Maybe ?
sTo? (nat n) = just …在Agda中,如何定义一对必须具有相同长度的向量？
-- my first try, but need to have 'n' implicitly
b : ? ( n : ? ) ? ? (Vec ? n) (? _ ? Vec ? n)
b 2 = (1 ? 2 ? []) , (3 ? 4 ? [])
b 3 = (1 ? 2 ? 3 ? []) , (4 ? 5 ? 6 ? [])
b _ = _
-- how can I define VecSameLength correctly?
VecSameLength : Set
VecSameLength = _
c …链接：具有Pyhton绑定的
Z3定理证明者
picosat
我已经使用Z3作为SAT求解器。对于较大的公式，似乎存在性能问题，这就是为什么我想查看picosat来查看它是否是更快的替代方案。我现有的python代码使用z3语法生成一个命题公式：
from z3 import *
import pycosat
from pycosat import solve, itersolve
#
#1 2 3 4 5 6 7 8 (variable names in picosat are numbers!)
#
C, G, M, P, R, S, SN, B = Bools('C G M P R S SN B')
C = (And(*(S,Or(Not(S),P),Or(Not(P),S),Or(Not(P),B),Or(Not(C),P),Or(Not(G),P),Or(Not(M),P),Or(Not(R),P),Or(Not(SN),P),Or(Not(B),P),True,Not(False),Or(R,SN,B,G,M,C,True))))
# formula in Z3:
f = simplify(C)
print f
输出/结果
And(S,
Or(Not(S), P),
Or(Not(P), S),
Or(Not(P), B),
Or(Not(C), P),
Or(Not(G), P),
Or(Not(M), P),
Or(Not(R), P),
Or(Not(SN), P),
Or(Not(B), …今天我也想看看在haskell中解决SAT的选项.首先,我想把自己的接口写入picosat求解器.
然后我发现有SBV库.它是Z3,Yices,CVC4和Boolector的接口.
此外,我在github上进行了谷歌搜索,它甚至可以使用Picosat绑定.
考虑到快速/高性能的限制,是否有任何其他针对SAT求解器的haskell绑定值得关注.Carification:适用于高性能SAT解决(例如,运行数天的问题,以及需要在检查2 ^ 20或更多SAT问题时尽快完成的问题).例如,我在hackage上特别缺少的是绑定到像Plingeling这样的快速并行 SAT求解器.(另外,我在github上发现了当前更新的picosat绑定更多的意外,我很可能会错过其他选项)
SBV库的默认选项是Z3 SMT解算器.在我受过良好教育的猜测中,我是否正确,对于简单的SAT解决而言,picosat比Z3更快？
不久前,"ATS"编程语言已从计算机语言基准游戏中删除.您仍然可以通过后机查看旧页面.
为什么ATS编程语言不再包含在计算机语言基准游戏中？