Scholarlink

<p>We present theoretical and practical results on the order theory of lattices of functions, focusing on Galois connections that abstract (sets of) functions – a topic known as <i>higher-order abstract interpretation</i>. We are motivated by the challenge of inferring closed-form bounds on functions which are defined recursively, i.e. as the fixed point of an operator or, equivalently, as the solution to a functional equation. This has multiple applications in program analysis (e.g. cost analysis, loop acceleration, declarative language analysis) and in hybrid systems governed by differential equations. Our main contribution is a new family of constraint-based abstract domains for abstracting numerical functions, <InlineEquation ID="IEq1"> <EquationSource Format="MATHML"><math> <mi mathvariant="fraktur">B</mi> </math></EquationSource> <EquationSource Format="TEX">$\mathfrak {B}$</EquationSource> </InlineEquation><i>-bound domains</i>, which abstract a function <InlineEquation ID="IEq2"> <EquationSource Format="MATHML"><math> <mi>f</mi> </math></EquationSource> <EquationSource Format="TEX">$f$</EquationSource> </InlineEquation> by a conjunction of bounds from a preselected set of boundary functions. They allow inferring <i>highly non-linear numerical invariants</i>, which classical numerical abstract domains struggle with. We uncover a <i>convexity property</i> in the constraint space that simplifies, and, in some cases, fully <i>automates</i>, transfer function design. We also introduce <i>domain abstraction</i>, a functor that lifts arbitrary mappings in value space to Galois connections in function space. This supports abstraction from symbolic to numerical functions (i.e. <i>size abstraction</i>), and enables dimensionality reduction of equations. We base our constructions of transfer functions on a simple <i>operator language</i>, starting with <i>sequences</i>, and extending to more general <i>functions</i>, including multivariate, piecewise, and non-discrete domains.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Abstractions of sequences, functions and operators

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2026年3月19日

查看全文
  • Louis Rustenholz,
  • Pedro Lopez-Garcia,
  • Manuel V. Hermenegildo

摘要

We present theoretical and practical results on the order theory of lattices of functions, focusing on Galois connections that abstract (sets of) functions – a topic known as higher-order abstract interpretation. We are motivated by the challenge of inferring closed-form bounds on functions which are defined recursively, i.e. as the fixed point of an operator or, equivalently, as the solution to a functional equation. This has multiple applications in program analysis (e.g. cost analysis, loop acceleration, declarative language analysis) and in hybrid systems governed by differential equations. Our main contribution is a new family of constraint-based abstract domains for abstracting numerical functions, B $\mathfrak {B}$ -bound domains, which abstract a function f $f$ by a conjunction of bounds from a preselected set of boundary functions. They allow inferring highly non-linear numerical invariants, which classical numerical abstract domains struggle with. We uncover a convexity property in the constraint space that simplifies, and, in some cases, fully automates, transfer function design. We also introduce domain abstraction, a functor that lifts arbitrary mappings in value space to Galois connections in function space. This supports abstraction from symbolic to numerical functions (i.e. size abstraction), and enables dimensionality reduction of equations. We base our constructions of transfer functions on a simple operator language, starting with sequences, and extending to more general functions, including multivariate, piecewise, and non-discrete domains.