小编Agn*_*yay的帖子

原始问题:问题2

在高度为500且宽度为10 ^ 5的矩形空间中,我们给出N个点.

我们应该找出最大的子矩形,其基部位于x轴上,并且不包含其正确内部的任何点(但可以在其边缘包含它们).

我尝试了一种O(宽度^ 2)算法:

#include <iostream>
#include <algorithm>

const int nWidth = 100000;
const int nHeight = 500;

int main(){

  int *nMaxHeights = new int[nWidth];
  std::fill (nMaxHeights, nMaxHeights+nWidth, nHeight);

  int N;
  std::cin >> N;
  for (int x,y,iii=0; iii < N; iii++){
    std::cin >> x >> y;
    nMaxHeights[x] = std::min(y+1, nMaxHeights[x]);
  }

  int maxArea = 0;
  for (int jjj,iii=0; iii < nWidth; iii++){
    for (jjj=iii; jjj < nWidth; jjj++){
      if (nMaxHeights[jjj] < nMaxHeights[iii])
        break;
    }
    maxArea = std::max((jjj-iii+1)*nMaxHeights[iii],maxArea); …

n-碳脂肪族烷烃是由n个节点组成的无根树,其中每个节点的程度最多为4.例如,请参阅此列表,列出一些低n值的列举.

我正在寻找一种算法来计算这种n-碳脂族烷烃的数量,给定n.

我已经在化学堆栈交换中看到了这一点.我还想过动态编程,即从较小的组件构建较大的图形,但我不能处理过多的相同异构体.

澄清:Carbons只是一个比喻.我不想考虑C16和C17的不稳定性,也不关心立体异构体

我试图用Haskell实现Braun树，定义如下：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}

data BraunTree (n :: Nat) a where
    Empty :: BraunTree 0 a
    Fork :: a -> BraunTree n a -> 
            BraunTree m a ->
            Either (n :~: m) (n :~: (m + 1)) ->
            BraunTree (n + m + 1) a

现在，我试图尝试如何“类型安全”地将内容插入此树。

insert …

我想阅读STDIN中换行符分隔的字符串列表,直到看到一个新行并且我想要一个类型的动作IO [String].这是我如何使用递归来做到这一点:

myReadList :: IO String
myReadList = go []
where 
    go :: [String] -> IO [String]   
    go l = do {
                 inp <- getLine;
                 if (inp == "") then 
                     return l;
                 else go (inp:l);
                }

然而,这种使用方法模糊了可读性,并且是一种非常普遍的模式,理想情况下,人们希望将其抽象出来.

所以,这是我的尝试:

whileM :: (Monad m) => (a -> Bool) -> [m a] -> m [a]
whileM p []     = return []
whileM p (x:xs) = do
    s <- x
    if p s
    then do
        l <- whileM p xs
        return (s:l) …

假设我想创建一个包含两个组件的网页,比如a Navbar和a Body.这两个组件不相互作用,可以独立开发.所以,我有两个榆树文件,每个文件都有以下组件:

type Model = ...

type Msg = ...

init : (Model, Cmd Msg)

update : Msg -> Model -> (Model, Cmd Msg)

view : Model -> Html Msg

假设它们都工作正常,我们如何组合它们来制作一个包含这两个组件的程序？

我试着写这样的东西:

type Model = {body : Body.Model , navbar : Navbar.Model}
type Msg = BodyMsg Body.Msg | NavbarMsg Navbar.Msg

view : Model -> Html Msg
view model = div [] [Body.view model.body, Navbar.view model.navbar]

update : Msg -> Model -> (Model, Cmd Msg)
update = ... …

我有以下定义

Inductive subseq : list nat -> list nat -> Prop :=
| empty_subseq : subseq [] []
| add_right : forall y xs ys, subseq xs ys -> subseq xs (y::ys)
| add_both : forall x y xs ys, subseq xs ys -> subseq (x::xs) (y::ys)
.

使用这个,我希望证明以下引理

Lemma del_l_preserves_subseq : forall x xs ys, subseq (x :: xs) ys -> subseq xs ys.

所以,我试着看看subseq (x :: xs) ys做的证明destruct H.

Proof.
  intros. induction H.

3 …

显然,Agda中有一些功能称为积极性检查,即使type-in-type启用也可以显然保持系统声音.

我很想知道这是什么,但是Agda手册没有回答这个问题,只解释了如何关闭它.

在午餐桌上,我无意中听到这是关于类型理论的极性,但这就是我所知道的.我没有在网上找到任何解释这个概念的东西以及为什么它有助于保持稳健性.任何可理解的解释将不胜感激.

显然,在Haskell中有一种称为无限类型的东西.

例如,当我尝试iterate concatGHCi时,我得到了这个:

*Main> iterate concat

<interactive>:24:9: error:
    • Occurs check: cannot construct the infinite type: a ~ [a]
      Expected type: [a] -> [a]
        Actual type: [[a]] -> [a]
    • In the first argument of ‘iterate’, namely ‘concat’
      In the expression: iterate concat
      In an equation for ‘it’: it = iterate concat
    • Relevant bindings include
        it :: [a] -> [[a]] (bound at <interactive>:24:1)

我的问题是,究竟什么是无限类型？它们如何适应类型理论以及我可以从哪些资源中了解它们？有没有允许无限类型的编程语言？