A Solution to the PoplMark Challenge Using de Bruijn Indices in Isabelle/HOL

We present a solution to the PoplMark challenge designed by Aydemir et al., which has as a goal the formalization of the meta-theory of System $\hbox{F}_{<:}$ . The formalization is carried out in the theorem prover Isabelle/HOL using an encoding based on de Bruijn indices. We start with a relatively simple formalization covering only the basic features of System $\hbox{F}_{<:}$ , and explain how it can be extended to also cover records and more advanced binding constructs. We also discuss different styles of formalizing the evaluation relation, and how this choice influences executability of the specification.     

A Head-to-Head Comparison of de Bruijn Indices and Names

Often debates about pros and cons of various techniques for formalising lambda-calculi rely on subjective arguments, such as de Bruijn indices are hard to read for humans or nominal approaches come close to the style of reasoning employed in informal proofs. In this paper we will compare four formalisations based on de Bruijn indices and on names from the nominal logic work, thus providing some hard facts about the pros and cons of these two formalisation techniques. We conclude that the relative merits of the different approaches, as usual, depend on what task one has at hand and which goals one pursues with a formalisation.     

基于编织法的de Bruijn序列差异性研究

由于de Bruijn序列具有周期最大、元素分布均衡、线性复杂度较高等良好的伪随机性质,因此在序列密码的研究领域中占有重要位置,其中de Bruijn序列的构造问题一直是研究的热点问题之一.目前已有多种构造de Bruijn序列的方法,而对于构造所得de Bruijn序列的差异性则相对研究较少,本文主要讨论基于编织法得到的de Bruijn序列的差异性.基于编织法,高杨等人给出了一种由一条n级de Bruijn序列来构造四条2n级de Bruijn序列的方法.由于这四条2n级de Bruijn序列由两条编织序列I1和I2唯一决定,因此de Bruijn序列的差异性可由这两条编织序列的差异性来刻画,而这两条编织序列的差异性又可以转化为两个指定映射的差异性.映射的差异性问题进一步可归结为对n长状态(e0e2…e2n-2)来源序列的研究,最终本文得到两个映射出现差异的充要条件,进而得到这两个映射的差异数和差异率2(2^n-1+1)^-1.据此可知,由编织法构造的编织序列的差异率随着级数的增大而减少.     

Clues to the hidden nature of de Bruijn sequences

Order n de Bruijn sequences are the period 2ⁿ binary sequences produced by an n stage feedback shift register. Theoretical results are summarized and data are presented for feedback functions, generator polynomials, linear spans, and autocorrelation properties of modified de Bruijn sequences.     

Transposing Arrays on Multicomputers Using de Bruijn Sequences

Transposing anN×Narray that is distributed row- or columnwise acrossP=Nprocessors is a fundamental communication task that requires time- consuming interprocessor communication. It is the underlying communication task for the fast Fourier transform of long sequences and multidimensional arrays. It is also the key communication task for certain weather and climate models. A parallel transposition algorithm is presented for hypercube and mesh connected multicomputers with programmable networks. The optimal scheduling of network transmissions is not unique and is known to be nontrivial. Here, scheduling is determined by a single de Bruijn sequence ofNbits. The elements in each processor are first preordered and then, in groups of log₂ Padjacent elements, either transmitted or not transmitted, depending on the corresponding bit in the de Bruijn sequence. The algorithm is optimal both in overall time and the time that any individual element is in the network. The results are extended to other communication tasks including shuffles, bit reversal, index reversal, and general index-digit permutation. The caseP≠Nand rectangular arrays with non-power-of-two dimensions are also discussed. Algorithms for mesh connected multicomputers are developed by embedding the hypercube in the mesh. The optimal implementation of the algorithms requires certain architectural features that are not currently available in the marketplace.     

SKoorde:一种基于de Bruijn图的高效P2P模型

Koorde是一种常数度分布式哈希表（DHT）,但它的定位策略有待改进以减少逻辑路由跳数,而且它存在着逻辑拓扑和物理拓扑失配的问题。在定位过程中采用最短路径路由策略以减少定位跳数．同时提出一种利用IP地址的特性来增强拓扑一致性的路由模型SKoorde。实验仿真表明,SKoorde的平均查询率和平均跳转比两项指标均优于改进前的Koorde,能够较好地提高路由效率。     

修正de Bruijn序列的线性复杂度研究

n级de Bruijn-0/1序列,就是从de Bruijn序列2ⁿ个状态中去除一个全0状态（记为de Bruijn-0）或全1状态（记为de Bruijn-1）而得到的周期为2ⁿ-1的序列。研究了de Bruijn-0和de Bruijn-1（记为de Bruijn-0/1）序列的线性复杂度特性,提出了相关的定理并给出了证明,同时给出了4~6级de Bruijn-0/1序列线性复杂度的统计数据。     

D2B: A de Bruijn based content-addressable network

We show that the de Bruijn graph is appropriate for maintaining dynamic connections, e.g., between the members of a P2P application who join and leave the system at their convenience. We describe the content-addressable network D2B, based on an overlay network preserving de Bruijn connections dynamically, and on a distributed hash table (DHT) supporting efficient publish and search procedures. The overlay network has constant expected degree, and any publish or search operation in the DHT takes a logarithmic expected number of steps.     

de Bruijn序列查寻表标签的末位基准构造法

de Bruijn序列结构是一个查寻表,其核心是它的表标签.因此构造出查寻表标签对于生成de Bruijn序列十分重要.本文给出一种m+1元n级de Bruijn序列查询表标签的末位基准构造法.方法一为末住复制构造法,即对大部分节点用构成该节点的串的末位字符拷贝值作为该节点的标签.方法二为末位分组构造法,即对大部分节点按构成该节点的串的末位字符值分成两组,第一组的标签设为定值,第二组的标签任取为第一组节点的末位值.这些方法构造的壹寻表标签数随着m,n增长而成指数式增长.但仍与定值构造法一样,在局部看是有效的,但与查寻表标签本身数目的惊人增长比较起来就很渺小.方法二与定值标签构造法比较其速度提高了关于m和n的指数式倍.     

基于PC端网站的移动阅读解决方案

针对PC端设计的网站在移动设备端直接显示时界面极不友好,而且有许多内容阅读者根本不感兴趣。针对这种情况,本文实现了一种基于PC端网站的移动阅读解决方案。首先通过c URL函数获取HTTP和HTTPS页面的HTML内容,然后从中提取读者感兴趣的数据并在移动端进行内容重构。在普通话水平测试成绩查询系统上所做的实验表明:内容重构之后移动端的显示效果远胜于移动端浏览器直接打开网站的显示效果,而且显示内容更精准。     

基于面向对象技术的自动状态机实现

首先讨论了通常所使用的面向过程的自动状态机（FSM）解决方法，然后提出了运用面向对象技术的状态图解决方案，并以此开发出电话语音查询系统。     

基于广度优先搜索的八数码问题解决方案

介绍了一种基于广度优先搜索的八数码问题解决方案.     

基于XML的应用层安全解决方案

随着XML技术越来越多地运用到网络应用中，对网络应用的安全提出了新的需求，文章首先讨论了应用层安全涉及的内容，然后提出了基于XML的解决方案，最后分析了该解决方案在XML网络应用中的优势。     

On the k-tuple domination of de Bruijn and Kautz digraphs

In a digraph G, a vertex u is said to dominate itself and vertices v such that (u,v) is an arc of G. For a positive integer k, a k-tuple dominating set D of a digraph is a subset of vertices such that every vertex is dominated by at least k vertices in D. The k-tuple domination number of a given digraph is the minimum cardinality of a k-tuple dominating set of the digraph. In this letter, we give the exact values of the k-tuple domination number of de Bruijn and Kautz digraphs.     

基于有效性函数的聚类算法

聚类作为一种无监督的学习方法,通常需要人为地提供聚类的簇数。在先验知识缺乏的情况下,通过人为指定聚类参数是不合实际的。近年来研究的聚类有效性函数（Cluster Validity Index） 用于估计簇的数目及聚类效果的优劣。本文提出了一种新的基于有效性指数的聚类算法,无需提供聚类的参数。算法每步合并两个簇,使有效性指数值增加最大或减小最少。本文运用引力模型度量相似度,对可能出现的异常点情况作均匀化的处理。实验表明,本文的算法能正确发现特定数据的簇个数,和其它聚类方法比较,聚类结果具有较低的错误率,并在效率上优于一般的基于有效性指数的聚类算法。     

基于Microsoft Office2000的电子商务解决方案

提出了基于Microsoft Office2000的电子商务解决方案及其原理、方法与步骤,并分析了其安全性与局限性,最后给出了一个应用实例,进一步阐明了其技术可行性。